Monadic second-order logic

{{Short description|Form of 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.<ref>{{cite book|first1=Bruno|last1=Courcelle|author1-link=Bruno Courcelle|first2=Joost|last2=Engelfriet| title=Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach| publisher=Cambridge University Press|date=2012-01-01|isbn=978-0521898331|url=http://dl.acm.org/citation.cfm?id=2414243|access-date=2016-09-15}}</ref> 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 predicates. However, MSO is the fragment in which second-order quantification is limited to monadic predicates (predicates having a single argument). This is often described as quantification over "sets" because monadic predicates are equivalent in expressive power to sets (the set of elements for which the predicate is true).

Monadic second-order logic is expressively equivalent to plural logic.

== 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 predicate constants (in this case the binary edge predicate <math>E(x, y)</math>), but quantification is restricted to be over monadic predicate variables only. In the variant considered in automata theory and the Büchi–Elgot–Trakhtenbrot theorem, all predicates, constant or variable, must be monadic, with the exceptions of equality (<math>=</math>) and ordering (<math><</math>) relations.

== Computational complexity of evaluation ==

Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be existential quantifiers, outside of any other part of the formula. The first-order quantifiers are not restricted. That is, one can speak of "there exists some ''x'', such that..." and "for all ''x'', we have..." where ''x'' is a term, but one can only speak of "there exists some monadic predicate ''P'', such that..." not "for all monadic predicate ''P'', we have...".

Fagin's theorem states that existential second-order logic (ESO) captures precisely the descriptive complexity of the complexity class NP. By analogy, the class of problems that may be expressed in existential monadic second-order logic has been called '''monadic NP'''. In other words, EMSO captures precisely the descriptive complexity of monadic NP (MNP).

In the logic of graphs, testing whether a graph is disconnected is in MNP, as the test can be represented by a formula that describes the existence of a proper subset of vertices with no edges connecting them to the rest of the graph. The complementary problem, testing whether a graph is connected, does not belong to monadic NP. That is, it is a problem in co-MNP \ MNP. By symmetry, graph disconnection testing is in MNP \ co-MNP, showing that neither complexity class contains the other.<ref>{{citation | last = Fagin | first = Ronald | author1-link = Ronald Fagin | journal = Zeitschrift für Mathematische Logik und Grundlagen der Mathematik | mr = 0371623 | pages = 89–96 | title = Monadic generalized spectra | volume = 21 | year = 1975| doi = 10.1002/malq.19750210112 }}.</ref><ref>{{citation | last1 = Fagin | first1 = R. | author1-link = Ronald Fagin | last2 = Stockmeyer | first2 = L. | author2-link = Larry Stockmeyer | last3 = Vardi | first3 = M. Y. | author3-link = Moshe Vardi | contribution = On monadic NP vs. monadic co-NP | doi = 10.1109/sct.1993.336544 | publisher = Institute of Electrical and Electronics Engineers | title = Proceedings of the Eighth Annual Structure in Complexity Theory Conference | year = 1993| s2cid = 32740047 }}.</ref> The addition of "monadic" makes the question easier. The analogous question, of whether NP = co-NP, is 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, this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a tree automaton<ref>{{Cite journal|last1=Thatcher|first1=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.<ref name=":0">{{Cite journal|last=Meyer|first=Albert R.|date=1975|editor-last=Parikh|editor-first=Rohit|editor-link=Rohit Parikh|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><ref name=":1" /> 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 variables, when the input data is a tree or has bounded treewidth, there are efficient enumeration algorithms 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|last1=Arnborg|first1=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 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|url-access=subscription}}</ref> As a consequence of this result, the following theories are decidable: * The monadic second-order theory of trees. * S1S, The monadic second-order theory with one successor (that is, of <math>\mathbb{N}</math>) * WS2S and WS1S, which restrict quantification to finite subsets (weak monadic second-order logic). ** By binary-coding natural numbers as finite subsets, addition is definable even in WS1S.

For each of these theories (S2S, S1S, WS2S, WS1S), the complexity of the decision problem is nonelementary.<ref name=":0" /><ref name=":1">{{Cite journal|last1=Stockmeyer|first1=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|url-access=subscription}}</ref> They could be obtained by performing a reduction of the emptiness problem of the star-free languages to WS1S.<ref>{{Cite thesis |last=Stockmeyer |first=Larry Joseph |title=The complexity of decision problems in automata theory and logic. |date=1974 |degree=PhD |publisher=Massachusetts Institute of Technology |url=https://dspace.mit.edu/handle/1721.1/15540}}</ref> The WS1S is specifically known to be TOWER-complete.<ref>{{Cite journal |last=Schmitz|first=Sylvain|date=2016-02-03|title=Complexity Hierarchies beyond Elementary|url=https://dl.acm.org/doi/10.1145/2858784|journal=ACM Transactions on Computation Theory|language=en|volume=8|issue=1|pages=1–36|doi=10.1145/2858784|arxiv=1312.5686|issn=1942-3454}}</ref>

=== Use of satisfiability of MSO on trees in verification === Monadic second-order logic of trees has applications in formal verification. Decision procedures for MSO satisfiability<ref>{{Cite journal|last1=Henriksen|first1=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.|editor4-link=Tiziana Margaria|editor5-last=Steffen|editor5-first=B.|title=Mona: Monadic second-order logic in practice|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|last1=Fiedor|first1=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|url-access=subscription}}</ref><ref>{{Cite journal|last1=Traytel|first1=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|url-access=subscription}}</ref> have been used to prove properties of programs manipulating linked data structures,<ref>{{Cite book|last1=Møller|first1=Anders|last2=Schwartzbach|first2=Michael I.|title=Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation |chapter=The pointer assertion logic engine |date=2001-05-01|chapter-url=https://doi.org/10.1145/378795.378851|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, and for symbolic reasoning in hardware verification.<ref>{{Cite journal|last1=Basin|first1=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|url-access=subscription}}</ref>

==References==

Category:Mathematical logic