Abstract state machines: verification problems and computational power

Nowack, Antje; Grädel, Erich

doi:938

Abstract state machines: verification problems and computational power

Nowack, Antje (Author)

2004

Verantwortlichkeitsangabevorgelegt von Antje Nowack

ImpressumAachen : Publikationsserver der RWTH Aachen University 2004

UmfangIV, 181 S.

Aachen, Techn. Hochsch., Diss., 2004

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2004-07-21

Online
URN: urn:nbn:de:hbz:82-opus-9383
URL: https://publications.rwth-aachen.de/record/52467/files/Nowack_Antje.pdf

Einrichtungen

Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Abstrakte Zustandsmaschine (Genormte SW) ; Verifikation (Genormte SW) ; Formale Methode (Genormte SW) ; Entscheidbarkeit (Genormte SW) ; Berechenbarkeit (Genormte SW) ; Program Slicing (Genormte SW) ; Informatik (frei) ; Abstract State Machines (frei) ; ASMs (frei) ; verification (frei) ; slicing (frei) ; quantum algorithms (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Abstract State Machines (ASMs) bilden die Basis einer Methode zur Software-Spezifikation, welche Vorteile informaler Methoden (Verstaendlichkeit und Ausfuehrbarkeit der Spezifikation) mit Vorteilen formaler Methoden (Genauigkeit sowie Anwendbarkeit mathematischer Methoden und Ergebnisse) vereint. Anwendungen dieser Methode motivieren zahlreiche Berechnungs- und Entscheidungsprobleme. Die hohe Ausdrucksstaerke ist einer der Vorteile der ASMs, jedoch fuehrt sie fast unmittelbar zu Unentscheidbarkeits- bzw. Nichtberechenbarkeitsergebnissen im uneingeschraenkten Fall. Folglich gelangt man recht schnell zu der Frage, ob es ausdrucksstarke Klassen von ASMs gibt, fuer welche Enscheidbarkeits- und Berechenbarkeitsergebnisse bewiesen werden koennen. Im ersten Teil dieser Arbeit wird eine solche Klasse eingefuehrt. Diese ASMs werden bewachte ASMs genannt. Die Idee aehnelt derjenigen des bewachten Fragments der Logik erster Stufe, fuer welches Erfuellbarkeit entscheidbar ist. Weiterhin wird die Ausdrucksstaerke dieser Klasse analysiert und bewiesen, dass sie ausdrucksstaerker ist als Datalog LITE und als das bewachte Fragment der Fixpunktlogik erster Stufe. Im zweiten Teil der Arbeit wird die Entscheidbarkeit des allgemeiner Verifikationsprobleme betrachtet. Dies entspricht der Frage, ob alle Berechnungen einer ASM eine Eigenschaft erfuellen. Aufgrund der Unentscheidbarkeit im allgemeinen Fall, muessen die ASMs und die Eigenschaften eingeschraenkt werden, um Entscheidbarkeit zu erhalten. Bewachte ASMs bilden die Basis einer entscheidbaren Instanz des allgemeinen Verifikationsproblems. An diese Betrachtungen schliesst sich die Frage an nach der Moeglichkeit, die Beschraenkungen der ASMs abzuschwaechen, falls das Ziel nicht in der automatischen Verifikation sondern in Konzepten besteht, die Verifikation, Debugging, Testen unterstuetzen. Eine solches Konzept ist Slicing fuer ASMs, welches im dritten Teil dieser Arbeit eingefuehrt wird. Die Idee entspricht derjenigen des Program Slicing, dessen Ziel ist, diejenigen Anweisungen eines Programms zu bestimmen, welche sein Verhalten an einer gegebenen Stelle beeinflussen. Diese Anweisungen bilden wiederum ein syntaktisch korrektes Programm, welches Slice genannt wird. Bisherige Arbeiten haben Programmiersprachen betrachtet, deren Konzept sich grundsaetzlich von ASMs unterscheidet. Obwohl das Konzept des Program Slicing nicht direkt auf ASMs erweitert werden kann, laesst sich ein entsprechendes Konzept fuer ASMs finden. Ein solcher Ansatz wird hier vorgestellt. Obwohl ein minimaler Slice im Allgemeinen nicht berechenbar ist, wird bewiesen, dass ein minimaler Slice fuer bewachte ASMs berechenbar ist. Dieses Ergebnis kann auf mehrere Arten erweitert werden. Einige Erweiterungen auf groessere Klassen von ASMs sowie weitere Varianten des Slicing-Begriffs werden vorgestellt. Im vierten Teil dieser Arbeit wird die Betrachtungsweise der ASMs etwas veraendert. ASMs werden nicht nur als Spezifikationsformalismus gesehen sondern als Berechnungsmodell. Die ASM-These besagt, dass jeder Algorithmus, gleich welcher Art, schrittweise und auf seinem natuerlichen Abstraktionsniveau durch eine ASM simuliert werden kann. Diese These wurde fuer sequentielle und parallele synchrone Algorithmen von grundlegenden Prinzipien abgeleitet. Das Hauptergebnis dieses Teils ist, dass die ASM-These auch fuer Quanten-Algorithmen gilt.

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.

Fulltext:
PDF
(additional files)