Deciding Monadic Second Order Logic over ω(omega)-Words by Specialized Finite Automata

Barth, Stephan (2016): Deciding Monadic Second Order Logic over ω(omega)-Words by Specialized Finite Automata. In: Ábrahám, Erika und Huisman, Marieke (Hrsg.): Integrated formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Programming and Software Engineering, Bd. 9681. Cham: Springer. S. 245-259

Abstract

Several automata models are each capable of describing all omega-regular languages. The most well-known such models are Buchi, 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 omega-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 well-suited model for efficiently deciding MSO over omega-words. Our experimental evaluation suggests that loop automata are indeed well suited for deciding MSO over omega-words efficiently.

• Dokumententyp: Buchbeitrag
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 978-3-319-33692-3; 978-3-319-33693-0
• Ort: Cham
• Sprache: Englisch