Next:
Inhalt
Modelchecking
Karsten Schmidt
Inhalt
1 Vorgeplänkel
1.1 Aktueller Stand der Vorlesung
1.2 Praktikum
1.3 Ziel und Inhalt des Ganzen
2 Vom System zum Petrinetz
2.1 Systeme
2.2 Verteilte Systeme
2.3 Informelle Einführung von Petrinetzen
2.4 Formale Definition von Petrinetzen
2.5 Beschränkt oder nicht beschränkt
2.6 Semantik
3 Temporale Logik
3.1 Syntax
3.2 Semantik
3.3 Fragmente von CTL*
3.4 Standardeigenschaften
3.5 Halbordnung gegen Interleaving
4 Modelchecking am Erreichbarkeitsgraphen
Generelles Vorgehen und einfache Fälle
4.2 Tiefe-Zuerst-Suche
Implementation der Suche für den AU-Operator
4.4 Implementation von CheckEU
5 Modelchecking mit Automaten
Büchi-Automaten
Automaten für Formeln
5.3 Modelchecking
Binäre Entscheidungsgraphen
Binäre Entscheidungsgraphen
6.2 Modelchecking mit Entscheidungsgraphen
6.3 Zeugen und Gegenbeispiele
Fairneß
7 Branching-Prozesse
7.1 Das Logikfragment
Der Branching-Prozeß
Erfüllbarkeitsmengen
Berechnung der Erfüllbarkeitsmenge für Literalkonjunktionen
8 Symmetrien
8.1 Symmetriebegriff
8.2 Symmetrisches Verhalten
8.3 Erzeugendensystem
8.4 Berechnung
8.5 Aufbau reduzierter Erreichbarkeitsgraphen
9 Suchraumeinengung
9.1 Definition von Transitionsauswahlen
9.2 Berechnung sturer Mengen
Transitionsauswahlen für unendliche Pfade
9.4 LTL ohne X
Reduzierte Graphen für LTL
Reduzierte Graphen für CTL
10 Zusammenfassung
Übersicht über das Stoffgebiet
A Petrinetze
B Temporale Logik
C Die Modelchecking-Verfahren
Suche im Erreichbarkeitsgraph
Büchi-Automaten
Entscheidungsgraphen
Halbordnungsmodelchecking
Schlußbemerkungen
Index
Next:
Inhalt
K. Schmidt
