The Automata Theory Package omega

In this paper we present omega, a package of algorithms from the theory of !-automata. It is a growing collection of procedures which at the moment encompasses constructions like: inclusion tests for regular !-languages, conversion of acceptance conditions, Safra's determinization algorithm, construction of strategies in infinite games. 1 Introduction There are by now several tools for basic automata theoretic algorithms, in particular in connection with finite semigroups. In the Kiel group of theoretical computer science, the AMoRE tool had been developed. Since around 1980, more and more applications of automata theory are connected with !-automata (automata on infinite words), for example in the verification of finite state programs (model checking). However, the nice and intricate algorithms of !-automata theory had not implemented yet; so even small case studies are difficult or impossible. In order to fill this gap, the library omega is under development in Kiel. In the course o..