Algorithms for omega-Automata and Applications in the Construction and Verification of Programs

DFG-Logo DFG-Project (Research cluster: "Efficient algorithms for discrete problems and their applications"):

Brief Description

The goal of this project is:

  1. to develop base algorithms for omega-automata, i.e. for transformation between different types of omega-automata; algorithms for reduction and minimizing omega-automata, for emptiness and inclusion tests, "model checking" and synthesis of I/O-automata,
  2. to extend algorithmic theory of omega-automata to structured omega-automata (modular specification), aiming to apply the available algorithms to specifications which occur in practice of industrial software development (Cooperation partner: ZT AN 1 Siemens),
  3. to implement algorithms for (1) and (2) as a public accessible software library,
  4. to develop methods of implementing algorithms over large transition graphs (e.g. state graphs of circuits or distributed systems); especially results on BDDs (binary decision diagrams), on partitioning, parallelization, and on alternative solutions (among others: discounted payoff-games with real parameters).


Further Related Publications

  • O. Matz, A. Miller, A. Potthoff, W. Thomas, E. Valkema: AMoRE (Automata, Monoids and Regular Expressions), Report on the Program AMoRE. Technical Report 9507, Institute of Computer Science and Applied Mathematics in the Christian-Albrecht-University of Kiel 1995.
  • A. Krompholz: Ein Policy Iteration Algorithmus für unendliche Spiele mit Rabin-Chain Akzeptierbedingung. Studienarbeit, Universität Kiel 1997.
  • B. Leoniuk: Akzeptierformeln für omega-Automaten und ihre Klassifizierung. Diplomarbeit, Kiel 1997.
  • H. Lescow: On polynomial-size strategies in finite-state games. In: Computer-Aided Verification (P. Wolper, Ed.), Springer LNCS 939 (1995), pages 239-252.
  • B. Leoniuk, H. Lescow, W. Thomas: Singleton acceptance conditions in omega-automata. Manuskript, Kiel 1997.
  • P. Johannsen: Ein Synthese-Verfahren für Controller in Realzeit-Systemen und seine Implementierung. Diplomarbeit, Kiel 1997.
  • M. Schimmler: Graphalgorithmen auf gitterverbundenen Prozessorfeldern. Dissertation, Ber. 9112, 153 S., Institut für Informatik und Praktische Mathematik, Universität Kiel 1991.
  • W. Thomas: Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 135-191. Elsevier, Amsterdam, 1990.
  • W. Thomas: On the synthesis of strategies in infinite games. In STACS 95, volume 900 of Lect. Notes in Comput. Sci., pages 1-13, Springer-Verlag, 1995.
  • W. Thomas: Languages, automata, and logic. In: Handbook of Formal Language Theory (G. Rozenberg, A. Salomaa, Eds.), Vol. III, Springer-Verlag, New York 1997.
  • W. Thomas, H. Lescow: Logical specification of infinite computations. In: "A Decade of Concurrency" (J.W. de Bakker et al., eds), Springer LNCS 803 (1994), pages 583-621.
  • Th. Wilke: An algebraic theory for regular languages of finite and infinite words. Intern. J. Algebra and Computation, 3(4):447-489, 1993.
  • Th. Wilke and H. Yoo: Computing the Wadge degree, the Lifshitz degree, and the Rabin index of a regular language of infinite words in polynomial time. In Trees in Algebra and Programming -- CAAP '95, volume 915 of Lect. Notes in Comput. Sci., pages 288-302, Springer-Verlag, 1995.