Tech Reports


Temporal Verification of Monodic Abstract State Machines

Michael Fisher and Alexei Lisitsa


particularly successful in specifying abstract algorithms, realistic programming languages, distributed computations, and a variety of different types of hardware. In this paper, we pursue the goal of automatic deductive verification of certain classes of ASM. In particular, we base our work on a translation of general ASMs to full first-order temporal logic. While such a logic is, in general, not finitely axiomatisable, recent work has identified a fragment, termed the monodic fragment, that is finitely axiomatisable. Thus, in this paper, we define a class of monodic ASMs whose semantics in terms of temporal logic fits within the monodic fragment. This, together with recent work on clausal resolution methods for monodic fragments, allows us to carry out temporal verification of properties of monodic ASMs.

[Full Paper]