Barth, Stephan
(2016):
Deciding Monadic Second Order Logic over ω(omega)Words by Specialized Finite Automata.
In: Ábrahám, Erika; Huisman, Marieke (eds.) :
Integrated formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 15, 2016, Proceedings. Programming and Software Engineering, Vol. 9681. Cham: Springer. pp. 245259

Full text not available from 'Open Access LMU'.
Abstract
Several automata models are each capable of describing all omegaregular languages. The most wellknown such models are Buchi, parity, Rabin, Streett, and Muller automata. We present deeper insights and further enhancements to a lesserknown 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 omegaregular 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 omegawords. Our experimental evaluation suggests that loop automata are indeed well suited for deciding MSO over omegawords efficiently.