Inhalt

• 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
• Index