A Logic for Non-deterministic Parallel Abstract State Machines

  • Flavio FerrarottiEmail author
  • Klaus-Dieter Schewe
  • Loredana Tec
  • Qing Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9616)


We develop a logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules.


Function Symbol Proof System Successor State Primary Part Abstract State Machine 
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.


  1. 1.
    Ågotnes, T., Walicki, M.: Complete axiomatisations of properties of finite sets. Logic J. IGPL 16(3), 293–313 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
  3. 3.
    Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms. ACM Trans. Comp. Logic 4(4), 578–651 (2003)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms: correction and extension. ACM Trans. Comp. Logic 9(3), 1–32 (2008)MathSciNetGoogle Scholar
  5. 5.
    Börger, E., Stärk, R.F.: Abstract State Machines: a Method for High-Level System Design and Analysis. Springer, New York (2003)CrossRefzbMATHGoogle Scholar
  6. 6.
    Ferrarotti, F., Schewe, K., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. CoRR abs/1504.06203 (2015).
  7. 7.
    Floyd, R.W.: Nondeterministic algorithms. J. ACM 14(4), 636–644 (1967). Google Scholar
  8. 8.
    Grädel, E., Gurevich, Y.: Metafinite model theory. Inf. Comput. 140(1), 26–81 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Groenboom, R., Renardel de Lavalette, G.: A formalization of evolving algebras. In: Proceedings of Accolade95. Dutch Research School in Logic (1995)Google Scholar
  10. 10.
    Huggins, J.K., Wallace, C.: An abstract state machine primer. Technical report 02–04, Computer Science Department, Michigan Technological University (2002)Google Scholar
  11. 11.
    Hughes, G., Cresswell, M.: A New Introduction to Modal Logic. Burns & Oates, London (1996)CrossRefzbMATHGoogle Scholar
  12. 12.
    Kruskal, J.B.: On the shortest spanning subtree of a graph and the travelling salesman problem. Proc. Amer. Math. Soc. 2, 48–50 (1956)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Stärk, R., Nanchen, S.: A logic for abstract state machines. J. Univ. Comput. Sci. 7(11) (2001)Google Scholar
  14. 14.
    Vapnik, V.N.: The Nature of Statistical Learning Theory. Springer, New York (1995)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Flavio Ferrarotti
    • 1
    Email author
  • Klaus-Dieter Schewe
    • 1
  • Loredana Tec
    • 1
  • Qing Wang
    • 2
  1. 1.Software Competence Center HagenbergHagenbergAustria
  2. 2.Research School of Computer ScienceThe Australian National UniversityCanberraAustralia

Personalised recommendations