A Logic for Abstract State Machines

By Robert F. Stärk, Stanislas Nanchen. Journal of universal computer science (Online), 2001

861 citations recorded by the source corpus.

We introduce a logic for sequential, non distributed Abstract State Machines. Unlike other logics for ASMs which are based on dynamic logic, our logic is based on atomic propositions for the function updates of transition rules. We do not assume that the transition rules of ASMs are in normal form, for example, that they concern distinct cases. Instead we allow structuring concepts of ASM rules including sequential composition and possibly recursive submachine calls. We show that several axioms that have been proposed for reasoning about ASMs are derivable in our system and that the logic is complete for hierarchical (non-recursive) ASMs.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/cda123d0bace1b4af76274786d45c0296e81051e