Effizienter Leerheitstest pro Zustand auf Büchi-Automaten

Abstract - Zusammenfassung

Um aus einer LTL-Formel einen Monitor für diese zu erzeugen, ist es ein gängiger Weg
zunächst aus der Formel einen Büchi-Automaten zu generieren und diesen in einen Mo-
nitor zu überführen. Im Zuge dieser Umwandlung ist es nötig, einen Leerheitstest pro
Zustand auf diesem Büchi-Automaten durchzuführen, der für jeden Zustand bestimmt,
ob der Automat von dort aus noch akzeptieren kann. Ziel dieser Arbeit ist die Entwick-
lung eines effizienten Algorithmus, der für alle Zustände eines Büchi-Automaten deren
Leerheit bestimmt und die Implementierung dieses Algorithmus im Projekt LamaConv
des Instituts für Softwaretechnik und Programmiersprachen der Universität zu Lübeck,
wo er für die Monitor-Erzeugung genutzt werden soll.

To generate a monitor from an LTL formula, it is a common way to first generate a Büchi
automaton from this formula and then converting it to a monitor. During this conversion,
it is necessary to perform an emptiness-per-state-check on this Büchi automaton, which
is determining for each state, whether the automaton can still accept out of this state.
Within this thesis there shall be developed an efficient algorithm for determining the
emptiness-per-state of a Büchi automaton. This algorithm shall also be implemented
into the project LamaConv of the Institute of Software Engineering and Programming
Languages of the University of Lübeck, where it can be used for monitor generation.