A Semantic Characterization of Unbounded-Nondeterministic Abstract State Machines
(2007)DOI: 10.1007/978-3-540-73859-6_17
Abstract
Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 8 Gurevich characterizes the class of sequential ASMs in a purely semantic way by five amazingly general and elegant axioms. In 9 this result is extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich^a€™s original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs.
