Abstract
We propose a systematic investigation of the (semi-) automatic verifiability of ASMs. As a first step, we put forward two verification problems concerning the correctness of ASMs and investigate the decidability and complexity of both problems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Blass and Y. Gurevich. Existential fixed-point logic. In E. Börger, editor, Computation Theory and Logic, volume 270 of Lecture Notes in Computer Science, pages 20–36. Springer-Verlag, 1987.
A. Blass and Y. Gurevich. The Linear Time Hierarchy Theorems for Abstract State Machines. Journal of Universal Computer Science, 3(4):247–278, 1997.
A. Blass, Y. Gurevich, and J. Van den Bussche. Abstract State Machines and Computationally Complete Query Languages. This volume.
A. Blass, Y. Gurevich, and S. Shelah. Choiceless Polynomial Time. Technical Report MSR-TR-99-08, Mircosoft Research, 1999.
E. Börger and J. Huggins. Abstract State Machines 1988-1998: Commented ASM Bibliography. Bulletin of the EATCS, 64:105–127, February 1998.
D. Beauquier and A. Slissenko. Verification of Timed Algorithms: Gurevich Abstract State Machines versus First Order Timed Logic. Technical Report TIK-Report 87, ETH Zürich, March 2000.
E. Börger. Why Use Evolving Algebras for Hardware and Software Enginee-ring? In M. Bartosek, J. Staudek, and J. Wiederman, editors, Proceedings of 22nd Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM’ 95), volume 1012 of Lecture Notes in Computer Science, pages 236–271. Springer Verlag, 1995.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic. ACM Trans. on Prog. Lang. and Sys., 8(2):244–263, April 1986.
G. Del Castillo and K. Winter. Model Checking Support for the ASM High-Level Language. Technical Report TR-RI-99-209, Universität-GH Pader-born, June 1999.
H. D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.
E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Hand-book of Theoretical Computer Science, volume B, pages 995–11072. Elsevier Science Publishers B.V., 1990.
A. Gargantini and E. Riccobene. Encoding Abstract State Machines in PVS. This volume.
E. Grädel and M. Spielmann. Logspace Reducibility via Abstract State Machines. In J. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods (FM’ 99), volume 1709 of Lecture Notes in Computer Science, pages 1738–1757. Springer-Verlag, 1999.
Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
Y. Gurevich. May 1997 Draft of the ASM Guide. Technical Report CSE-0TR-336-97, University of Michigan, May 1997.
Y. Gurevich. The Sequential ASM Thesis. Bulletin of the EATCS, 67:93–124, 1999.
N. Immerman and M.Y. Vardi. Model Checking and Transitive Closure Logic. In Proceedings of 9th International Conference on Computer-Aided Verification (CAV’ 97), volume 1254 of Lecture Notes in Computer Science, pages 291–302. Springer-Verlag, 1997.
A. Levy, I. Mumick, Y. Sagiv, and O. Shmueli. Equivalence, Query-Reachability, and Satisfiaability in Datalog Extensions. In Proceedings of 12th ACM Symposium on Principles of Database Systems (PODS’ 93), pages 109–122, 1993.
E. Rosen. An existential fragment of second order logic. Archive for Mathematical Logic, 38:217–234, 1999.
A.P. Sistla and E.M. Clarke. The Complexity of Propositional Linear Temporal Logics. Journal of the Association for Computing Machinery, 32(3):733–749, July 1985.
M. Spielmann. Automatic Verification of Abstract State Machines. In Proceedings of 11th International Conference on Computer-Aided Verification (CAV’ 99), volume 1633 of Lecture Notes in Computer Science, pages 431–442. Springer-Verlag, 1999.
M. Spielmann. Verification of Relational Transducers for Electronic Commerce. In Proceedings of 19th ACM Symposium on Principles of Database Systems (PODS 2000). ACM Press, 2000. To appear.
M. Spielmann. Abstract State Machines: Verification Problems and Complexity. PhD thesis, RWTH Aachen. In preparation.
K. Winter. Model Checking for Abstract State Machines. Journal of Universal Computer Science, 3(5):689–701, 1997.
K. Winter. Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study. This volume.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Spielmann, M. (2000). Model Checking Abstract State Machines and Beyond. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds) Abstract State Machines - Theory and Applications. ASM 2000. Lecture Notes in Computer Science, vol 1912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44518-8_18
Download citation
DOI: https://doi.org/10.1007/3-540-44518-8_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67959-2
Online ISBN: 978-3-540-44518-0
eBook Packages: Springer Book Archive