LTL Muster für ProB

Temporale Logiken wie LTL sind oftmals schwer zugänglich, insbesondere wenn sie länger werden. Zum Schreiben von LTL-Formeln wurden daher Muster entwickelt ("LTL Patterns"), in der sich Sachverhalte wie "Bevor A passiert, muss B passieren" leicht ausdrücken lassen und die sich wiederum in LTL-Formeln übersetzen lassen.

Ziel einer Arbeit währe eine konkrete Umsetzung für den ProB Modelchecker, die eine benutzerfreundliche Bearbeitung von Mustern erlaubt.