|
| publisher = Institute of Electrical and Electronics Engineers
| title = Proceedings of the Eighth Annual Structure in Complexity Theory Conference
| year = 1993| s2cid = 32740047 }}.</ref> The existence of an analogous pair of complementary problems, only one of which has an existential second-order formula (without the restriction to monadic formulas) is equivalent to the inequality of NP and [[coNP]], an open question in computational complexity.
By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finite [[tree (data structure)|tree]], this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a [[tree automaton]]<ref>{{Cite journal|lastlast1=Thatcher|firstfirst1=J. W.|last2=Wright|first2=J. B.|date=1968-03-01|title=Generalized finite automata theory with an application to a decision problem of second-order logic|journal=Mathematical Systems Theory|language=en|volume=2|issue=1|pages=57–81|doi=10.1007/BF01691346|s2cid=31513761|issn=1433-0490|ref=ThatcherWright}}</ref> and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generally [[nonelementary problem|nonelementary]].<ref name=":0">{{Cite journal|last=Meyer|first=Albert R.|date=1975|editor-last=Parikh|editor-first=Rohit|title=Weak monadic second order theory of {{sic|succes|or|hide=y}} is not elementary-recursive|journal=Logic Colloquium|series=Lecture Notes in Mathematics|language=en|publisher=Springer Berlin Heidelberg|pages=132–154|doi=10.1007/bfb0064872|isbn=9783540374831}}</ref> Thanks to [[Courcelle's theorem]], we can also evaluate a Boolean MSO formula in linear time on an input graph if the [[treewidth]] of the graph is bounded by a constant.
For MSO formulas that have [[free variable]]s, when the input data is a tree or has bounded treewidth, there are efficient [[enumeration algorithm]]s to produce the set of all solutions,<ref>{{Cite journal|last=Bagan|first=Guillaume|date=2006|editor-last=Ésik|editor-first=Zoltán|title=MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay|journal=Computer Science Logic|volume=4207|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=167–181|doi=10.1007/11874683_11|isbn=9783540454595}}</ref> ensuring that the input data is preprocessed in linear time and that each solution is then produced in a delay linear in the size of each solution, i.e., constant-delay in the common case where all free variables of the query are first-order variables (i.e., they do not represent sets). There are also efficient algorithms for counting the number of solutions of the MSO formula in that case.<ref>{{Cite journal|lastlast1=Arnborg|firstfirst1=Stefan|last2=Lagergren|first2=Jens|last3=Seese|first3=Detlef|date=1991-06-01|title=Easy problems for tree-decomposable graphs|journal=Journal of Algorithms|volume=12|issue=2|pages=308–340|doi=10.1016/0196-6774(91)90006-K|issn=0196-6774}}</ref>
== 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 [[decidability (logic)|decidable]].<ref>{{Cite journal|last=Rabin|first=Michael O.|date=1969|title=Decidability of Second-Order Theories and Automata on Infinite Trees|url=https://www.jstor.org/stable/1995086|journal=Transactions of the American Mathematical Society|volume=141|pages=1–35|doi=10.2307/1995086|jstor=1995086|issn=0002-9947}}</ref> As a consequence of this result, the following theories are decidable:
* The monadic second-order theory of trees.
* The monadic second order theory of <math>\mathbb{N}</math> 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 problem|nonelementary]].<ref name=":0" /><ref>{{Cite journal|lastlast1=Stockmeyer|firstfirst1=Larry|last2=Meyer|first2=Albert R.|date=2002-11-01|title=Cosmological lower bound on the circuit complexity of a small problem in logic|url=https://doi.org/10.1145/602220.602223|journal=Journal of the ACM|volume=49|issue=6|pages=753–784|doi=10.1145/602220.602223|s2cid=15515064|issn=0004-5411}}</ref>
=== Use of satisfiability of MSO on trees in verification ===
Monadic second-order logic of trees has applications in [[Software verification]] and, more broadly, [[Formal verification]] thanks to its decidability and significant expressive power. Decision procedures for satisfiability have been implemented.<ref>{{Cite journal|lastlast1=Henriksen|firstfirst1=Jesper G.|last2=Jensen|first2=Jakob|last3=Jørgensen|first3=Michael|last4=Klarlund|first4=Nils|last5=Paige|first5=Robert|last6=Rauhe|first6=Theis|last7=Sandholm|first7=Anders|date=1995|editor-last=Brinksma|editor-first=E.|editor2-last=Cleaveland|editor2-first=W. R.|editor3-last=Larsen|editor3-first=K. G.|editor4-last=Margaria|editor4-first=T.|editor5-last=Steffen|editor5-first=B.|title=Mona: Monadic second-order logic in practice|url=https://link.springer.com/chapter/10.1007/3-540-60630-0_5|journal=Tools and Algorithms for the Construction and Analysis of Systems|series=Lecture Notes in Computer Science|volume=1019|language=en|___location=Berlin, Heidelberg|publisher=Springer|pages=89–110|doi=10.1007/3-540-60630-0_5|isbn=978-3-540-48509-4|doi-access=free}}</ref><ref>{{Cite journal|lastlast1=Fiedor|firstfirst1=Tomáš|last2=Holík|first2=Lukáš|last3=Lengál|first3=Ondřej|last4=Vojnar|first4=Tomáš|date=2019-04-01|title=Nested antichains for WS1S|url=https://doi.org/10.1007/s00236-018-0331-z|journal=Acta Informatica|language=en|volume=56|issue=3|pages=205–228|doi=10.1007/s00236-018-0331-z|s2cid=57189727|issn=1432-0525}}</ref><ref>{{Cite journal|lastlast1=Traytel|firstfirst1=Dmitriy|last2=Nipkow|first2=Tobias|date=2013-09-25|title=Verified decision procedures for MSO on words based on derivatives of regular expressions|url=https://doi.org/10.1145/2544174.2500612|journal=ACM SIGPLAN Notices|volume=48|issue=9|pages=3–f12|doi=10.1145/2544174.2500612|issn=0362-1340|hdl=20.500.11850/106053|hdl-access=free}}</ref> Such procedures were used to prove properties of programs manipulating linked data structures,<ref>{{Cite journal|lastlast1=Møller|firstfirst1=Anders|last2=Schwartzbach|first2=Michael I.|date=2001-05-01|title=The pointer assertion logic engine|url=https://doi.org/10.1145/378795.378851|journal=Proceedings of the ACM SIGPLAN 2001 conferenceConference on Programming languageLanguage designDesign and implementationImplementation|series=PLDI '01|___location=Snowbird, Utah, USA|publisher=Association for Computing Machinery|pages=221–231|doi=10.1145/378795.378851|isbn=978-1-58113-414-8|s2cid=11476928}}</ref> as a form of [[Shape analysis (program analysis)|Shape analysis]] as well as for symbolic reasoning in hardware verification.<ref>{{Cite journal|lastlast1=Basin|firstfirst1=David|last2=Klarlund|first2=Nils|date=1998-11-01|title=Automata based symbolic reasoning in hardware verification|url=https://doi.org/10.1023/A:1008644009416|journal=Formal Methods in System Design|volume=13|issue=3|pages=255–288|doi=10.1023/A:1008644009416|issn=0925-9856}}</ref>
==See also==
| 