State-space reduction of finite automata with applications in the verification of non-terminating systems

• Applicant: Professor Dr. Thomas Wilke
• Subject Area: Theoretical Computer Science
• Term: from 2001 to 2007
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5330154

• Final Report Year: 2006

Final Report Abstract

Im Rahmen des Vorhabens wurde der Ansatz, den Zustandsraum endlicher Automaten durch Quotientenbildung nach Simulationsrelationen zu reduzieren, auf weitere, aus der Verifikation motivierte Automatenmodelle übertragen. So wurden Simulationsrelationen und geeignete Quotientenkonstruktionen für alternierende Büchi-Wortautomaten, Paritätsspiele und alternierende Paritätswortautomaten eingeführt. Darüberhinaus wurden zum einen die dafür notwendigen Theorien und zum anderen effiziente Algorithmen zur Berechnung der eingeführten Simulationsrelationen entwickelt. Des Weiteren entstanden Algorithmen (Heuristiken), die eine effizientere Umsetzung von Formeln aus Spezifikationslogiken (lineare temporale Logik, modales u-Kalkül) in möglichst kleine äquivalente Automaten ermöglichen. Obwohl die Algorithmen zur Reduktion der Größe von Paritätsspielen eine hohe Zustandsreduktion erreichen, sind sie langsamer als Algorithmen, die Paritätsspiele direkt lösen. Der spieltheoretische Ansatz zur Definition von Simulationsrelationen, der durchweg benutzt wurde, hat sich als sehr hilfreich und vielseitig erwiesen.

Publications

• State Space Reductions for Alternating Büchi Automata. In: Agrawal, Manindra und Anil Seth (Herausgeber): FSTTCS, Band 2556 der Reihe Lecture Notes in Computer Science, Seiten 157-168. Springer, 2002.
  Fritz, Carsten und Thomas Wilke
  
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata. In: Ibarra, Oscar H. und Zhe Dang (Herausgeber): CIAA, Band 2759 der Reihe Lecture Notes in Computer Science, Seiten 35-48. Springer, 2003.
  Fritz, Carsten
  
• Games 2003, Jahrestreffen des EU RTN »Games and Automata for Synthesis and Validation«, Wien, 30. August - 2. September 2003
  
  
• LPAR 2003, 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Almaty, Kasachstan, 22. - 26. September 2003.
  
  
• Concepts of Automata Construction from LTL. In: Sutcliffe, Geoff und Andrei Voronkov (Herausgeber): LPAR, Band 3835 der Reihe Lecture Notes in Computer Science, Seiten 728-742. Springer, 2005.
  Fritz, Carsten
  
• Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata. SIAM J. Comput, 34(5):1159-1175. 2005.
  Etessami, Kousha, Thomas Wilke und Rebecca A. Schuller
  
• Simulation relations for alternating Büchi automata. Theor. Comput. Sei., 338(l-3):275-314, 2005.
  Fritz, Carsten und Thomas Wilke
  
• Simulation Relations for Alternating Parity Automata and Parity Games. In: Ibarra, Oscar H. und Zhe Dang (Herausgeber): Developments in Language Theory, Band 4036 der Reihe Lecture Notes in Computer Science, Seiten 59-70. Springer, 2006.
  Fritz, Carsten und Thomas Wilke
  
• Simulation-based simplification of omega-automata. Doktorarbeit, Technische Fakultät, Christian-Albrechts-Universität zu Kiel, 2006.
  Fritz, Carsten