Modal Extensions of the Logic of Abstract State Machines

Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension ML ASM by first introducing multi-step predicates and then adding quantification over the number of steps. We show that liveness conditions such as invariance, conditional and unconditional progress, and persistence on all or some runs of an ASM can be expressed in this logic. We show the existence of a complete fragment of MLASM, which still contains the interesting liveness conditions, and demonstrate the usefulness of this complete fragment by an example concerning mutual exclusion.