A logic for non-deterministic parallel abstract state machines

F. Ferrarotti, Q. Wang. A logic for non-deterministic parallel abstract state machines. volume 9616, pages 334-354, DOI 10.1007/978-3-319-30024-5_18, 3, 2016.

Autoren
  • Flavio Ferrarotti
  • Qing Wang
BuchFoundations of Information and Knowledge Systems - Proc. FoIKS 2016
TypIn Konferenzband
VerlagSpringer
SerieLecture Notes in Computer Science
Band9616
DOI10.1007/978-3-319-30024-5_18
ISBN978-3-319-30023-8
Monat3
Jahr2016
Seiten334-354
Abstract

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.