Model Checking Abstract State Machines and Beyond

  • Marc Spielmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)


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.


Model Check Temporal Logic Turing Machine Initialization Mapping Computation Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.CrossRefGoogle Scholar
  2. 2.
    A. Blass and Y. Gurevich. The Linear Time Hierarchy Theorems for Abstract State Machines. Journal of Universal Computer Science, 3(4):247–278, 1997.MathSciNetzbMATHGoogle Scholar
  3. 3.
    A. Blass, Y. Gurevich, and J. Van den Bussche. Abstract State Machines and Computationally Complete Query Languages. This volume.Google Scholar
  4. 4.
    A. Blass, Y. Gurevich, and S. Shelah. Choiceless Polynomial Time. Technical Report MSR-TR-99-08, Mircosoft Research, 1999.Google Scholar
  5. 5.
    E. Börger and J. Huggins. Abstract State Machines 1988-1998: Commented ASM Bibliography. Bulletin of the EATCS, 64:105–127, February 1998.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    H. D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    A. Gargantini and E. Riccobene. Encoding Abstract State Machines in PVS. This volume.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.Google Scholar
  15. 15.
    Y. Gurevich. May 1997 Draft of the ASM Guide. Technical Report CSE-0TR-336-97, University of Michigan, May 1997.Google Scholar
  16. 16.
    Y. Gurevich. The Sequential ASM Thesis. Bulletin of the EATCS, 67:93–124, 1999.MathSciNetzbMATHGoogle Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    E. Rosen. An existential fragment of second order logic. Archive for Mathematical Logic, 38:217–234, 1999.MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    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.Google Scholar
  21. 21.
    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.zbMATHGoogle Scholar
  22. 22.
    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.Google Scholar
  23. 23.
    M. Spielmann. Abstract State Machines: Verification Problems and Complexity. PhD thesis, RWTH Aachen. In preparation.Google Scholar
  24. 25.
    K. Winter. Model Checking for Abstract State Machines. Journal of Universal Computer Science, 3(5):689–701, 1997.zbMATHGoogle Scholar
  25. 26.
    K. Winter. Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study. This volume.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Marc Spielmann
    • 1
  1. 1.Mathematische Grundlagen der InformatikRWTH AachenAachenGermany

Personalised recommendations