Bearbeiter: offen
Aufgabensteller: Prof. Dr. Alexander Knapp
Betreuer: Moritz Hammer.
Vorkenntnisse: Kenntnisse in (linearer) Temporallogik.

Eine LTL-Formel f heisst endlich widerlegbar wenn ein Gegenbeispiel einen endlichen Präfix hat, so dass alle Ergänzungen zu unendlichen Pfaden ebenfalls Gegenbeispiele sind. Beispielsweise ist eine Formel [] a endlich widerlegbar, wie das Gegenbeispiel !a a a ... zeigt. Endlich widerlegbare Formeln eignen sich zum Kontrollieren von Software, indem sie als Monitor verwendet haben und prüfen, ob eine beobachtete Sequenz von z.B. Kommunikationsschritten der Formel noch genügt.

Im Rahmen des Fortgeschrittenenpraktikums soll die Klasse der endlich widerlegbaren Formeln untersucht werden. Darüber hinaus ist denkbar, Wege der "endlich-widerlegbar"-Machung von Formeln, z.B. durch die Annotation mit Realzeit-Konstraints zu untersuchen.