Untersuchung der Klasse der endlich widerlegbaren LTL-Formeln
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.
