Verification of Weighted Timed Automata
Final Report Abstract
In diesem Projekt, angesiedelt im Gebiet der Theoretischen Informatik (genauer: Formale Verifikation), wurden Entscheidungsprobleme von gewichteten Zeitautomaten untersucht. Gewichtete Zeitautomaten eignen sich zur Modellierung von Echtzeitsystemen, in denen Ressourcen wie Energie, Geld, u.ä. produziert und konsumiert werden. Viele Entscheidungsprobleme sind unentscheidbar wenn die Automaten es erlauben Ressourcen zu modellieren, die sich kontinuierlich, in Abhängigkeit von der Zeit, andern können. Deswegen haben wir uns im Projekt auf die Betrachtung von gewichteten Zeitautomaten über diskreten Ressourcenstrukturen beschränkt. In solchen Automaten kann die Ressourcenvariable eine rein beobachtende Rolle einnehmen, z.B. wenn man an der Modellierung von Optimierungsproblemen interessiert ist. Die Ressourcenvariable kann aber auch das Verhalten des Automaten aktiv beeinflussen; beispielsweise kann man mit solchen Ressourcenvariablen Systeme modellieren, in denen eine Ressource einen bestimmten Wert nicht über- oder unterschreiten darf. Im Projekt haben wir erfolgreich einige interessante, der Verifikation von Echtzeitsystemen dienliche Entscheidungsprobleme untersucht, nicht nur für Zeitautomaten, sondern auch für verwandte unendliche Transitionssysteme wie Zählerautomaten oder Registerautomaten. Unter anderem haben wir folgende Ergebnisse erzielt: • Das sogenannte Pfad-Checking Problem für die Temporallogik MTL. Wir beweisen, dass dieses Problem, wichtig für die Laufzeitanalyse von Einzählerautomaten, handhabbar ist. • Das Synchronisierungsproblem für Registerautomaten. Dieses Problem steht im Zusammenhang mit der Anforderung Systeme, die mit Daten aus unendlichen Domänen operieren, “resetten” zu können. Wir zeigen, dass das Problem im Allgemeinen unentscheidbar ist; im Falle deterministischer Systeme sowie längenbeschränkter Resetwörter können wir jedoch Entscheidbarkeit beweisen. • Die Definierbarkeit der Erreichbarkeitsrelation von Zeitautomaten. Wir vereinfachen ein bekanntes Resultat von Comon und Jurski. Auf Basis dieses Resultats entwickeln wir einen EXPSPACE-Algorithmus zum Model Checking von Zeitautomaten gegen Formeln einer parametrisierten Echtzeittemporallogik. • Das Erreichbarkeitsproblem von parametrisierten Einzählerautomaten. Wir zeigen NP-Vollständigkeit; hierzu entwickeln wir neue und einfache Techniken, von denen wir glauben, dass sie sich auch für die Analyse anderer Systeme eignen. • Das Enthaltenseinproblem für eindeutige Registerautomaten. Wir entwickeln neuartige Techniken um zu zeigen, dass dieses Problem in 2EXPSPACE entscheidbar ist.
Publications
- Path Checking for MTL and TPTL. In Developments in Language Theory (DLT 2015), S. 326-339, Springer LNCS, Volume 9168, 2015
Karin Quaas, S. Feng und M. Lohrey
(See online at https://doi.org/10.1007/978-3-319-21500-6_26) - Verification for Timed Automata extended with Discrete Data Structure. In Logical Methods in Computer Science, Vol. 11(3), 2015
Karin Quaas
(See online at https://doi.org/10.1007/978-3-662-44584-6_35) - Synchronizing Data Words for Register Automata. . In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), S. 15:1-15:15, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016
Karin Quaas, P. Babari und M. Shirmohammadi
(See online at https://doi.org/10.4230/LIPIcs.MFCS.2016.15) - An Algebraic Approach to Energy Problems II - The Algebra of Energy Functions. In Acta Cybernetica. Volume 23, S. 229-268, 2017
Karin Quaas, Z. Ésik, U. Fahrenberg und A. Legay
(See online at https://doi.org/10.14232/actacyb.23.1.2017.14) - In Thirty-Second ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), S. 1-12, IEEE Computer Society, 2017
Karin Quaas, Worrell und M. Shirmohammadi
(See online at https://doi.org/10.1109/LICS.2017.8005098) - Path Checking for MTL and TPTL over Data Words. In Logical Methods in Computer Science, Vol. 13(3), 2017
Karin Quaas, M. Lohrey und S. Feng
(See online at https://doi.org/10.23638/LMCS-13(3:19)2017) - The Complexity of Flat Freeze LTL. In 28th Conference on Concurrency Theory (CONCUR 2017), S. 33:1–33:16, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017
Karin Quaas, B. Bollig und A. Sangnier
(See online at https://doi.org/10.4230/LIPIcs.CONCUR.2017.33) - The Containment Problem for Unambiguous Register Automata
Karin Quaas, A. Mottet
