A Guarded Fragment for Abstract State Machines
Mathematische Grundlagen der Informatik · 2005
Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results. In this work, we introduce such a class of ASMs. The concept is similar to the one of the guarded fragment of first-order logic. We analyze the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works. Abstract State Machines (ASMs) have been introduced as an attempt to bridge the gap between formal models of computation and practical specification methods. The result is a formal method for transparent design and specification of complex dynamic systems. ASMs combine advantages of informal methods (understandabil- ity, executability) with advantages of formal methods (precision and applicability of mathematical methods and results). On the one hand, the ASM method is a formal method. There is a precise semantics allowing the application of mathematical methods to analyze ASMs. In particular, these are often results from mathematical logic as ASMs use classical mathematical structures to describe states of a computation. Anyhow, ASMs are easily understandable. ASM specifications are easy to read and to write. And this is one of the most important (pre)conditions for a broad acceptance in practice and a resulting application. The reason for the understand- ability is that ASMs have a very simple syntax that is quite similar to pseudo-code. And indeed, ASMs are used in practice to specify hardware and software systems. Reports on this can be found e.g. in Borger et al. (2000) and Stark et al. (2001).