Automata-Theoretic Techniques in Probabilistic Verification

Kontakt

Anton Pirogov

Telefon

work
+49 241 80 21707

E-Mail

E-Mail
 

Probabilistische Verifikation beschäftigt sich mit Fragen wie z.B. nach der Wahrscheinlichkeit für die Erfüllung von bestimmten Korrektheitskriterien im Bezug auf das Verhalten von Softwaresystemen. Solche Kriterien werden in einer formalen Logik ausgedrückt und auf einer geeigneten repräsentativen Abstraktion des Systems überprüft. Zur Lösung von Fragestellungen aus der formalen Verifikation sind automatenbasierte Techniken oft das Mittel der Wahl, da diese oft gut algorithmisch handhabbar sind. Das Ziel dieses Dissertationsprojektes ist die Verbesserung solcher Techniken, insbesondere:

- Verbesserung der Determinisierung von Omega-Automaten durch Entwicklung neuer Algorithmen und Heuristiken

- Erforschung von neuen geeigneten Automatenmodellen zur Anwendung im probabilistischen Model-Checking

Die Ergebnisse dieses Projektes werden sich unmittelbar auf die Praktikabilität von automatenbasiertem Model-Checking auswirken, die stark von der Größe und Komplexität der verwendeten Automaten abhängt.