Deciding monadic second order logic over ω-words by specialized finite Automata

Abstract

Several automata models are each capable of describing all ω-regular languages. The most well-known such models are Büchi, parity, Rabin, Streett, and Muller automata. We present deeper insights and further enhancements to a lesser-known model. This model was chosen and the enhancements developed with a specific goal: Decide monadic second order logic (MSO) over infinite words more efficiently. MSO over various structures is of interest in different applications, mostly in formal verification. Due to its inherent high complexity, most solvers are designed to work only for subsets of MSO. The most notable full implementation of the decision procedure is MONA, which decides MSO formulae over finite words and trees. To obtain a suitable automaton model, we further studied a representation of ω-regular languages by regular languages, which we call loop automata. We developed an efficient algorithm for homomorphisms in this representation, which is essential for deciding MSO. Aside from the algorithm for homomorphism, all algorithms for deciding MSO with loop automata are simple. Minimization of loop automata is basically the same as minimization of deterministic finite automata. Efficient minimization is an important feature for an efficient decision procedure for MSO. Together this should theoretically make loop automata a wellsuited model for efficiently deciding MSO over ω-words. Our experimental evaluation suggests that loop automata are indeed well suited for deciding MSO over ω-words efficiently.