20-00-1115-vl Model Checking

Lehrende: Dr. rer. nat. Richard Bubel

Veranstaltungsart: Vorlesung

Orga-Einheit: FB20 Informatik

Anzeige im Stundenplan: MC

Fach:

Anrechenbar für:

Semesterwochenstunden: 2

Unterrichtssprache: Englisch

Min. | Max. Teilnehmerzahl: - | -

Digitale Lehre:
Der Kurs wird auf Englisch gehalten.
Die Kurswebseite ist:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1201

Lehrinhalte:

• Temporallogiken - Lineare temporal Logik (LTL), Computation Tree Logic (CTL) und CTL*: Syntax, Semantik, Komplexität
  
• Modelprüfungsverfahren für LTL, CTL, CTL*, insbesondere Büchiautomaten
  
• Partial Order Reduction
  
• Timed Automata
  

Voraussetzungen:
Kenntnisse in

• Aussagenlogik
  
• Deduktionssystemen
  
• Automatentheorie
  

Zusätzliche Informationen:
Kurswebseite:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1201

Online-Angebote:
Kurswebseite:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1201