Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec, Qing Wang,
"A Logic for Non-deterministic Parallel Abstract State Machines"
: Proceedings of the 9th International Symposium on Foundations of Information and Knowledge Systems - Volume 9616, Serie FoIKS 2016, Vol. 9616, Springer-Verlag New York, Inc., New York, NY, USA, Seite(n) 334--354, 2016, ISBN: 978-3-319-30023-8
A Logic for Non-deterministic Parallel Abstract State Machines
Sprache des Titels:
Proceedings of the 9th International Symposium on Foundations of Information and Knowledge Systems - 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.