A Logic for Abstract State Machines

A Logic for Abstract State Machines

2001 | Robert F. Stärk, Stanislas Nanchen
The paper introduces a logic for non-distributed, deterministic Abstract State Machines (ASMs) with parallel function updates. Unlike other logics for ASMs, which are based on dynamic logic, this logic is based on an atomic predicate for function updates and a definedness predicate for the termination of transition rule evaluations. The logic allows for structuring concepts of ASM rules, including sequential composition and recursive submachine calls. The authors show that several axioms proposed for reasoning about ASMs are derivable in their system. They also provide an extension of the logic with explicit step information, which allows for the elimination of modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs, and it is shown that for these ASMs, the logic is a definitional extension of first-order predicate logic. The paper includes a detailed introduction to ASMs, formalizes the consistency of ASMs, and presents the basic axioms and rules of the logic. It also discusses the limitations of non-deterministic ASMs and concludes with a proof of completeness for hierarchical ASMs.The paper introduces a logic for non-distributed, deterministic Abstract State Machines (ASMs) with parallel function updates. Unlike other logics for ASMs, which are based on dynamic logic, this logic is based on an atomic predicate for function updates and a definedness predicate for the termination of transition rule evaluations. The logic allows for structuring concepts of ASM rules, including sequential composition and recursive submachine calls. The authors show that several axioms proposed for reasoning about ASMs are derivable in their system. They also provide an extension of the logic with explicit step information, which allows for the elimination of modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs, and it is shown that for these ASMs, the logic is a definitional extension of first-order predicate logic. The paper includes a detailed introduction to ASMs, formalizes the consistency of ASMs, and presents the basic axioms and rules of the logic. It also discusses the limitations of non-deterministic ASMs and concludes with a proof of completeness for hierarchical ASMs.
Reach us at info@study.space