Exact Exploration and Hanging Algorithms

Abstract. Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sealgorithm, there is an abstract state machine (ASM) with the same states, initial states and state transitions. That analysis, however, abstracted from details of intra-step computation, and the ASM, produced in the proof of the representation theorem, may and often does explore parts of the state unexplored by the algorithm. We refine the analysis, the axiomatization and the representation theorem. Emulating a step of the given algorithm, the ASM, produced in the proof of the new representation theorem, explores exactly the part of the state explored by the algorithm. That frugality pays off when state exploration is costly. The algorithm may be a high-level specification, and a simple function call on the abstraction level of the algorithm may hide expensive interaction with the environment. Furthermore, the original analysis presumed that state ...

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Andreas Blass, Nachum Dershowitz, Yuri Gurevich
• Keywords: Abstract State Machine, Algorithm, Automated Reasoning, CSL 2010, Representation Theorem