Abstract state machines: verification problems and computational power

Abstract State Machines (ASMs) provide the basis of a a formal method combining advantages of informal methods (understandability, executability) and advantages of formal methods (precision and applicability of mathematical methods and results). Applications of this method motivate numerous computability and decidability problems. The high expressive power is one of the advantages of ASMs but it leads rather directly to undecidability respectively uncomputability results in the unrestricted case. Consequently, we arrive rather early at the question whether there exist expressive classes of ASMs for which we can prove decidability and computability results. In the first part of this thesis, we introduce such a class called guarded ASMs. The idea is similar to the one of the guarded fragment of first-order logic for which satisfiability is decidable. We analyze the expressive power of this class and prove that it is (strictly) stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. In the second part of this thesis, we study the decidability of general verification problems for ASMs corresponding to the question whether all computations of an ASM satisfy a property (usually expressed in some temporal logic). Because of undecidability in the general case, we have to restrict the ASMs and the properties in order to obtain decidability results. Guarded ASMs provide the basis of a decidable instance of the general verification problem. It is rather straightforward to ask for the possibility to weaken the restrictions on the ASMs if we do not aim automatic verification but concepts supporting verification, debugging and testing. One such possibility is the concept of slicing ASMS which we introduce in the third part of this work. The idea is analogous to the one of program slicing aiming to extract statements from a program that are relevant for its behavior at a given point of interest. These statements form again a syntactically correct program called a slice. Previous work has focused on programming languages that differ substantially from ASMs. Although the concept of program slicing does not directly extend to ASMs, it is possible to find an analogous concept for ASMs. We present such an approach. In spite of the fact that a minimal slice is not computable in the general case, we prove that a minimal slice is computable for guarded ASMs. This basic result can be extended in several ways. We present some extensions to larger classes of ASMs and other variants for the notion of slicing. In the fourth part of this thesis, we change our point of view. We do not merely consider ASMs as a specification formalism but as a computation model. The ASM thesis says that every algorithm, of any kind, can be modeled step by step and on its natural abstraction level by an ASM. The thesis has been derived from basic principles for sequential algorithms, and for parallel synchronous algorithms. The main result of this part is that the ASM thesis also holds for quantum algorithms.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2004

Author dc:creator

• Nowack, Antje

Contributors dc:contributor

• Grädel, Erich

• info:eu-repo/classification/ddc/004
• Abstrakte Zustandsmaschine
• Verifikation
• Formale Methode
• Entscheidbarkeit
• Berechenbarkeit
• Program Slicing
• Informatik
• Abstract State Machines
• ASMs
• verification
• slicing
• quantum algorithms

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-114688%22

OAI record oai:identifier

https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A52467