A unifying logic for non-deterministic, parallel and concurrent abstract state machines

F. Ferrarotti, K. Schewe, L. Tec, Q. Wang. A unifying logic for non-deterministic, parallel and concurrent abstract state machines. Annals of Mathematics and Artificial Intelligence, pages online first, DOI 10.1007/s10472-017-9569-3, 12, 2017.

Autoren
  • Flavio Ferrarotti
  • Klaus-Dieter Schewe
  • Loredana Tec
  • Qing Wang
TypArtikel
JournalAnnals of Mathematics and Artificial Intelligence
DOI10.1007/s10472-017-9569-3
ISSN1573-7470 (electronic version)
Monat12
Jahr2017
Seitenonline first
Abstract

We develop a logic which enables reasoning about single steps of non-deterministic and 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 within the logical formalism. We do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic and parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules. Moreover, we show that the proposed one-step logic can be easily extended to a multiple-step logic which enables reasoning about concurrent ASMs.