Formal language theory is an elegant tool used in many fields of computer science. In particular, languages over infinite words are a convenient tool to model reactive systems and hence find applications to verification and synthesis. In these applications, the correctness of algorithms is crucial. Thus, it is important to have trustworthy algorithms on languages.
Often, the most important problem is to decide language equality or inclusion, because many other problems can be reduced to it. For example, in model checking, a system and a given specification can both be represented as languages. These languages are then tested for language inclusion to check if the system matches the specification. Similarly, system equivalence can be reduced to language equivalence.
Languages can be represented in many ways, including, for example, automata, logics and expressions. Automata and logics have already been studied extensively, including in proof assistants, resulting in a variety of trustworthy algorithms to decide equivalence on them. Omega-regular expressions, however, have been considered much less and are to our knowledge not yet formalized in a proof assistant. In contrast to automata, omega-regular expressions can be modified and manipulated syntactically. They are also more compact and easier to reason about, especially in a proof assistant. In particular, it is possible to use structural induction, a powerful reasoning tool, on expressions. Despite these advantages, there are so far no algorithms to decide equivalence for omega-regular expressions without translating them to some other representation.
In this work, we study the semantics of omega-regular expressions in the Coq proof assistant as well as develop a new (and first to our knowledge) algorithm for deciding equivalence directly on omega-regular expressions. Furthermore, we formalize the algorithm in Coq and verify it. The equivalence checker is proven sound, but not complete, and extracted to an executable OCaml program.