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.
Item Type: | Book Section |
---|---|
Faculties: | Mathematics, Computer Science and Statistics > Computer Science |
Subjects: | 000 Computer science, information and general works > 004 Data processing computer science |
ISBN: | 978-3-319-33692-3; 978-3-319-33693-0 |
Place of Publication: | Cham |
Language: | English |
Item ID: | 47333 |
Date Deposited: | 27. Apr 2018, 08:12 |
Last Modified: | 04. Nov 2020, 13:24 |