Monadic second-order logic
In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets.[1] It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.
Second-order logic allows quantification over
Variants
Monadic second-order logic comes in two variants. In the variant considered over structures such as graphs and in Courcelle's theorem, the formula may involve non-monadic predicates (in this case the binary edge predicate ), but quantification is restricted to be over monadic predicates only. In the variant considered in automata theory and the Büchi–Elgot–Trakhtenbrot theorem, all predicates, including those in the formula itself, must be monadic, with the exceptions of equality () and ordering () relations.
Computational complexity of evaluation
Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be
By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finite
For MSO formulas that have
Decidability and complexity of satisfiability
The satisfiability problem for monadic second-order logic is undecidable in general because this logic subsumes first-order logic.
The monadic second-order theory of the infinite complete binary tree, called S2S, is decidable.[8] As a consequence of this result, the following theories are decidable:
- The monadic second-order theory of trees.
- The monadic second-order theory of under successor (S1S).
- WS2S and WS1S, which restrict quantification to finite subsets (weak monadic second-order logic). Note that for binary numbers (represented by subsets), addition is definable even in WS1S.
For each of these theories (S2S, S1S, WS2S, WS1S), the complexity of the decision problem is nonelementary.[5][9]
Use of satisfiability of MSO on trees in verification
Monadic second-order logic of trees has applications in
See also
References
- ISBN 978-0521898331. Retrieved 2016-09-15.
- MR 0371623.
- S2CID 32740047.
- S2CID 31513761.
- ^ ISBN 9783540374831.
- ISBN 9783540454595.
- ISSN 0196-6774.
- JSTOR 1995086.
- S2CID 15515064.
- ISBN 978-3-540-48509-4.
- S2CID 57189727.
- ISSN 0362-1340.
- S2CID 11476928.
- ISSN 0925-9856.