Monadic second-order logic: Difference between revisions

Revision as of 14:52, 23 May 2019

Revision as of 18:59, 31 May 2019

Line 1:

In [[mathematical logic]], '''monadic second -order logic''' ('''MSO)''') is the fragment of [[Second-order logic|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|accessdate=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]].

Second-order logic allows quantification over [[Predicate (mathematical logic)|predicates]]. However, MSO is the [[Fragment (logic)|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).

Line 22:

| year = 1993}}.</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|last=Thatcher|first=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|url=https://doi.org/10.1007/BF01691346|journal=Mathematical systems theory|language=en|volume=2|issue=1|pages=57–81|doi=10.1007/BF01691346|issn=1433-0490}}</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>{{Cite journal|last=Meyer|first=Albert R.|date=1975|editor-last=Parikh|editor-first=Rohit|title=Weak monadic second order theory of succesor{{sic|succes|or|hide=y}} is not elementary-recursive|url=https://link.springer.com/chapter/10.1007%2FBFb0064872|journal=Logic Colloquium|series=Lecture Notes in Mathematics|language=en|publisher=Springer Berlin Heidelberg|pages=132–154|doi=10.1007/bfb0064872.pdf|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|url=https://link.springer.com/chapter/10.1007/11874683_11|journal=Computer Science Logic|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|last=Arnborg|first=Stefan|last2=Lagergren|first2=Jens|last3=Seese|first3=Detlef|date=1991-06-01|title=Easy problems for tree-decomposable graphs|url=http://www.sciencedirect.com/science/article/pii/019667749190006K|journal=Journal of Algorithms|volume=12|issue=2|pages=308–340|doi=10.1016/0196-6774(91)90006-K|issn=0196-6774}}</ref>