2007/07/31 by Andreas Blass, Yuri Gurevich, Dean Rosenzweig +1 · 29 citations
Computer Science · Mathematics · #Algorithm #Basis (linear algebra) #Computability, Logic, AI Algorithms #Computer science #Cover (algebra) #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #State (computer science) #Theoretical computer science #cs.LO
paper · pdf · doi:10.2168/lmcs-3(4:3)2007
published in Logical Methods in Computer Science Volume 3, Issue 4 (Logical Methods in Computer Science e.V.)
arxiv created 2007/11/05 · openalex publication_date 2007/11/05 · arxiv updated 2015/07/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
In earlier work, the Abstract State Machine Thesis -- that arbitrary algorithms are behaviorally equivalent to abstract state machines -- was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. Here we extend the axiomatization and, in a companion paper, the proof, to cover interactive small-step algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment's replies but also the order in which the replies were received.