Abstract state machines [Elektronische Ressource] : verification problems and computational power / vorgelegt von Antje Nowack

Antje Nowack

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2004
• Nombre de lectures: 18
• Langue: Deutsch

Extrait

Abstract State Machines:
Veri cation Problems and
Computational Power
Von der Fakulatt fur Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westf alischen Technischen
Hochschule Aachen zur Erlangung des akademischen Grades einer
Doktorin der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatikerin
Antje Nowack
aus Dusse ldorf
Berichter: Universit atsprofessor Dr. Erich Gradel
Universit a Dr. Wolfgang Thomas
Tag der mundlic hen Prufung: 21. Juli 2004
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfugba r.Zusammenfassung
Abstract State Machines (ASMs) bilden die Basis einer Methode zur Software-
Spezi kation, welche Vorteile informaler Methoden (Verstandlichkeit und Aus-
fuhrba rkeit der Spezi kation) mit Vorteilen formaler Methoden (Genauigkeit
sowie Anwendbarkeit mathematischer Methoden und Ergebnisse) vereint. An-
wendungen dieser Methode motivieren zahlreiche Berechnungs- und Entschei-
dungsprobleme. DiehoheAusdrucksst arkeisteinerderVorteilederASMs,jedoch
fuhrt sie fast unmittelbar zu Unentscheidbarkeits- bzw. Nichtberechenbarkeit-
sergebnissenimuneingeschranktenFall. Folglichgelangtmanrechtschnellzuder
Frage,obesausdrucksstarkeKlassenvonASMsgibt,fur welcheEnscheidbarkeits-
und Berechenbarkeitsergebnisse bewiesen werden k onnen. Im ersten Teil dieser
Arbeit wird eine solche Klasse eingefuhrt. Diese ASMs werden bewachte ASMs
genannt. Die Idee ahnelt derjenigen des bewachten Fragments der Logik er-
ster Stufe, fur welches Erfullbar keit entscheidbar ist. Weiterhin wird die Aus-
drucksst arke dieser Klasse analysiert und bewiesen, da sie ausdrucksst arker ist
als Datalog LITE und als das bewachte Fragment der Fixpunktlogik erster Stufe.
Im zweiten Teil der Arbeit wird die Entscheidbarkeit des allgemeiner Veri-
kationsprobleme betrachtet. Dies entspricht der Frage, ob alle Berechnungen
einer ASM eine Eigenschaft erfullen. Aufgrund der Unentscheidbarkeit im allge-
meinen Fall, mussen die ASMs und die Eigenschaften eingeschr ankt werden, um
Entscheidbarkeit zu erhalten. Bewachte ASMs bilden die Basis einer entscheid-
baren Instanz des allgemeinen Veri kationsproblems.
An diese Betrachtungen schliet sich die Frage an nach der M oglichkeit, die
Beschr ankungen der ASMs abzuschw achen, falls das Ziel nicht in der automa-
tischen Veri kation sondern in Konzepten besteht, die Veri kation, Debugging,
Testen unterstutze n. Eine solches Konzept ist Slicing fur ASMs, welches im drit-
tenTeildieserArbeiteingefuhr twird. DieIdeeentsprichtderjenigendesProgram
Slicing, dessen Ziel ist, diejenigen Anweisungen eines Programms zu bestimmen,
welche sein Verhalten an einer gegebenen Stelle beein ussen. Diese Anweisun-
gen bilden wiederum ein syntaktisch korrektes Programm, welches Slice genannt
wird. BisherigeArbeitenhabenProgrammiersprachenbetrachtet,derenKonzept
sich grundsatzlich von ASMs unterscheidet. Obwohl das Konzept des Program
Slicingnichtdirektauferweitertwerdenkann,al tsicheinentsprechendes
Konzept fur ASMs nden. Ein solcher Ansatz wird hier vorgestellt. Obwohl ein
minimaler Slice im Allgemeinen nicht berechenbar ist, wird bewiesen, da einler Slice fur bewachte ASMs berechenbar ist. Dieses Ergebnis kann auf
mehrere Arten erweitert werden. Einige Erweiterungen auf gr o ere Klassen von
ASMs sowie weitere Varianten des Slicing-Begri s werden vorgestellt.
Im vierten Teil dieser Arbeit wird die Betrachtungsweise der ASMs etwas
ver andert. ASMs werden nicht nur als Spezi kationsformalismus gesehen son-
dern als Berechnungsmodell. Die ASM-These besagt, da jeder Algorithmus,
gleich welcher Art, schrittweise und auf seinem naturlic hen Abstraktionsniveau
durch eine ASM simuliert werden kann. Diese These wurde fur sequentielle und
parallele synchrone Algorithmen von grundlegenden Prinzipien abgeleitet. Das
HauptergebnisdiesesTeilsist,dadieASM-Theseauchfur Quanten-Algorithmen
gilt.Abstract
Abstract State Machines (ASMs) provide the basis of a a formal method com-
biningadvantagesofinformalmethods(understandability, executability)andad-
vantagesofformalmethods(precisionandapplicabilityofmathematicalmethods
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 uncomputabili-
ty 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 rst part of this thesis, we intro-
duce such a class called guarded ASMs. The idea is similar to the one of the
guardedfragmentof rst-orderlogicforwhichsatisabilityisdecidable. Weana-
lyze the expressive power of this class and prove that it is (strictly) stronger than
Datalog LITE and the guarded fragment of rst-order xed point logic.
Inthesecondpartofthisthesis,westudythedecidabilityofgeneralveri cation
problemsforASMscorrespondingtothequestionwhetherallcomputationsofan
ASM satisfy a property (usually expressed in some temporal logic). Because of
undecidabilityinthegeneralcase,wehavetorestricttheASMsandtheproperties
in order to obtain decidability results. Guarded ASMs provide the basis of a
decidable instance of the general veri cation problem.
It is rather straightforward to ask for the possibility to weaken the restrictions
on the ASMs if we do not aim automatic veri cation but concepts supporting
veri cation, 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 di er substantially from ASMs. Although the
concept of program slicing does not directly extend to ASMs, it is possible to
nd 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 speci cation 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 de-
rivedfrombasicprinciplesforsequentialalgorithms, andforparallelsynchronous
algorithms. The main result of this part is that the ASM thesis also holds for
quantum algorithms.Acknowledgements
Iwanttothankallpeoplewhocontributeddirectlyorindirectlytothisthesis. In
particular, I want to thank my advisor, Professor Erich Gradel, for his support
and guidance during the last years. Furthermore, I want to thank Professor
Wolfgang Thomas for his kind readiness to write the second report on this thesis.Contents
Introduction 1
Basic De nitions of Abstract State Machines 9
Examples of Abstract State Machines 17
Modelling a Simple Algorithm . . . . . . . . . . . . . . . . . . . . . . . 17
Simulation of a Turing Machine . . . . . . . . . . . . . . . . . . . . . . 17
I Guarded Abstract State Machines 21
1 Exploiting Concepts from Mathematical Logic 23
1.1 Classical Decidable Fragments of First-Order Logic . . . . . . . . 23
1.2 Guarded Fragments . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2 Computational Power of Guarded Abstract State Machines 29
2.1 Basic Properties of Guarded ASMs . . . . . . . . . . . . . . . . . 30
2.2 Guarded ASMs are Stronger than Datalog LITE . . . . . . . . . . 32
2.3 ASMs are Stronger than Guarded Fixed Point Logic . . 37
II Veri cation 47
3 Verifying and Speci ying Properties of Abstract State Machines 49
3.1 The Veri cation Problem . . . . . . . . . . . . . . . . . . . . . . . 49
3.2 Specifying Properties of Abstract State Machines . . . . . . . . . 50
3.2.1 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . 50
3.2.2 Branching Time Logic . . . . . . . . . . . . . . . . . . . . 51
4 Simple Restrictions 55
4.1 Simple Classes of Abstract State Machines . . . . . . . . . . . . . 55
4.2 Decidability Results . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.2.1 Hennessy-Milner First-Order Logic . . . . . . . . . . . . . 56
4.2.2 First-Order CTL . . . . . . . . . . . . . . . . . . . . . . . 61
iii Contents
4.3 Undecidability Results . . . . . . . . . . . . . . . . . . . . . . . . 65
4.4 Remarks and Conclusion . . . . . . . . . . . . . . . . . . . . . . . 69
5 Known Advanced Decidability Results 71
5.1 Nullary Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.2 ASM transducers . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6 A Class of Guarded Abstract State Machines 75
6.1 De nition and a Normal Form . . . . . . . . . . . . . . . . . . . . 75
6.2 Logical Background . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.3 Deciding the General Veri cation Problem . . . . . . . . . . . . . 79
6.4 Complexit