Monadic second-order logic

Last updated

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.

Contents

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).

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 existential quantifiers, outside of any other part of the formula. The first-order quantifiers are not restricted. By analogy to Fagin's theorem, according to which existential (non-monadic) second-order logic captures precisely the descriptive complexity of the complexity class NP, the class of problems that may be expressed in existential monadic second-order logic has been called monadic NP. The restriction to monadic logic makes it possible to prove separations in this logic that remain unproven for non-monadic second-order logic. For instance, in the logic of graphs, testing whether a graph is disconnected belongs to monadic NP, 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; however, the complementary problem, testing whether a graph is connected, does not belong to monadic NP. [2] [3] 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, this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a tree automaton [4] and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generally nonelementary. [5] 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, [6] 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. [7]

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:

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 formal verification. Decision procedures for MSO satisfiability [10] [11] [12] have been used to prove properties of programs manipulating linked data structures, [13] as a form of shape analysis, and for symbolic reasoning in hardware verification. [14]

See also

Related Research Articles

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.

<span class="mw-page-title-main">Monochromatic triangle</span>

In graph theory and theoretical computer science, the monochromatic triangle problem is an algorithmic problem on graphs, in which the goal is to partition the edges of a given graph into two triangle-free subgraphs. It is NP-complete but fixed-parameter tractable on graphs of bounded treewidth.

Fagin's theorem is the oldest result of descriptive complexity theory, a branch of computational complexity theory that characterizes complexity classes in terms of logic-based descriptions of their problems rather than by the behavior of algorithms for solving those problems. The theorem states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP.

In graph theory, the treewidth of an undirected graph is an integer number which specifies, informally, how far the graph is from being a tree. The smallest treewidth is 1; the graphs with treewidth 1 are exactly the trees and the forests. The graphs with treewidth at most 2 are the series–parallel graphs. The maximal graphs with treewidth exactly k are called k-trees, and the graphs with treewidth at most k are called partial k-trees. Many other well-studied graph families also have bounded treewidth.

In graph theory, a path decomposition of a graph G is, informally, a representation of G as a "thickened" path graph, and the pathwidth of G is a number that measures how much the path was thickened to form G. More formally, a path-decomposition is a sequence of subsets of vertices of G such that the endpoints of each edge appear in one of the subsets and such that each vertex appears in a contiguous subsequence of the subsets, and the pathwidth is one less than the size of the largest set in such a decomposition. Pathwidth is also known as interval thickness, vertex separation number, or node searching number.

In computational complexity theory, SNP is a complexity class containing a limited subset of NP based on its logical characterization in terms of graph-theoretical properties. It forms the basis for the definition of the class MaxSNP of optimization problems.

In database theory, a conjunctive query is a restricted form of first-order queries using the logical conjunction operator. Many first-order queries can be written as conjunctive queries. In particular, a large part of queries issued on relational databases can be expressed in this way. Conjunctive queries also have a number of desirable theoretical properties that larger classes of queries do not share.

<span class="mw-page-title-main">Clique-width</span> Measure of graph complexity

In graph theory, the clique-width of a graph G is a parameter that describes the structural complexity of the graph; it is closely related to treewidth, but unlike treewidth it can be small for dense graphs. It is defined as the minimum number of labels needed to construct G by means of the following 4 operations :

  1. Creation of a new vertex v with label i (denoted by i(v))
  2. Disjoint union of two labeled graphs G and H (denoted by )
  3. Joining by an edge every vertex labeled i to every vertex labeled j (denoted by η(i,j)), where i ≠ j
  4. Renaming label i to label j (denoted by ρ(i,j))
<span class="mw-page-title-main">Ronald Fagin</span> American mathematician and computer scientist

Ronald Fagin is an American mathematician and computer scientist, and IBM Fellow at the IBM Almaden Research Center. He is known for his work in database theory, finite model theory, and reasoning about knowledge.

In graph theory, a Trémaux tree of an undirected graph is a type of spanning tree, generalizing depth-first search trees. They are defined by the property that every edge of connects an ancestor–descendant pair in the tree. Trémaux trees are named after Charles Pierre Trémaux, a 19th-century French author who used a form of depth-first search as a strategy for solving mazes. They have also been called normal spanning trees, especially in the context of infinite graphs.

In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form

In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and independently rediscovered by Borie, Parker & Tovey (1992). It is considered the archetype of algorithmic meta-theorems.

In mathematical logic, the spectrum of a sentence is the set of natural numbers occurring as the size of a finite model in which a given sentence is true.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

<i>k</i>-outerplanar graph

In graph theory, a k-outerplanar graph is a planar graph that has a planar embedding in which the vertices belong to at most concentric layers. The outerplanarity index of a planar graph is the minimum value of for which it is -outerplanar.

In formal language theory, the Büchi–Elgot–Trakhtenbrot theorem states that a language is regular if and only if it can be defined in monadic second-order logic (MSO): for every MSO formula, we can find a finite-state automaton defining the same language, and for every finite-state automaton, we can find an MSO formula defining the same language. The theorem is due to Julius Richard Büchi, Calvin Elgot, and Boris Trakhtenbrot.

In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by Rabin in 1969.

References

  1. ↑ Courcelle, Bruno; Engelfriet, Joost (2012-01-01). Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press. ISBN   978-0521898331 . Retrieved 2016-09-15.
  2. ↑ Fagin, Ronald (1975), "Monadic generalized spectra", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21: 89–96, doi:10.1002/malq.19750210112, MR   0371623 .
  3. ↑ Fagin, R.; Stockmeyer, L.; Vardi, M. Y. (1993), "On monadic NP vs. monadic co-NP", Proceedings of the Eighth Annual Structure in Complexity Theory Conference, Institute of Electrical and Electronics Engineers, doi:10.1109/sct.1993.336544, S2CID   32740047 .
  4. ↑ Thatcher, J. W.; Wright, J. B. (1968-03-01). "Generalized finite automata theory with an application to a decision problem of second-order logic". Mathematical Systems Theory. 2 (1): 57–81. doi:10.1007/BF01691346. ISSN   1433-0490. S2CID   31513761.
  5. 1 2 Meyer, Albert R. (1975). Parikh, Rohit (ed.). "Weak monadic second order theory of succesor is not elementary-recursive". Logic Colloquium. Lecture Notes in Mathematics. Springer Berlin Heidelberg: 132–154. doi:10.1007/bfb0064872. ISBN   9783540374831.
  6. ↑ Bagan, Guillaume (2006). Ésik, Zoltán (ed.). "MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay". Computer Science Logic. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 4207: 167–181. doi:10.1007/11874683_11. ISBN   9783540454595.
  7. ↑ Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991-06-01). "Easy problems for tree-decomposable graphs". Journal of Algorithms. 12 (2): 308–340. doi:10.1016/0196-6774(91)90006-K. ISSN   0196-6774.
  8. ↑ Rabin, Michael O. (1969). "Decidability of Second-Order Theories and Automata on Infinite Trees". Transactions of the American Mathematical Society . 141: 1–35. doi:10.2307/1995086. ISSN   0002-9947. JSTOR   1995086.
  9. ↑ Stockmeyer, Larry; Meyer, Albert R. (2002-11-01). "Cosmological lower bound on the circuit complexity of a small problem in logic". Journal of the ACM . 49 (6): 753–784. doi:10.1145/602220.602223. ISSN   0004-5411. S2CID   15515064.
  10. ↑ Henriksen, Jesper G.; Jensen, Jakob; Jørgensen, Michael; Klarlund, Nils; Paige, Robert; Rauhe, Theis; Sandholm, Anders (1995). Brinksma, E.; Cleaveland, W. R.; Larsen, K. G.; Margaria, T.; Steffen, B. (eds.). "Mona: Monadic second-order logic in practice". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 1019: 89–110. doi: 10.1007/3-540-60630-0_5 . ISBN   978-3-540-48509-4.
  11. ↑ Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš (2019-04-01). "Nested antichains for WS1S". Acta Informatica. 56 (3): 205–228. doi:10.1007/s00236-018-0331-z. ISSN   1432-0525. S2CID   57189727.
  12. ↑ Traytel, Dmitriy; Nipkow, Tobias (2013-09-25). "Verified decision procedures for MSO on words based on derivatives of regular expressions". ACM SIGPLAN Notices. 48 (9): 3–f12. doi:10.1145/2544174.2500612. hdl: 20.500.11850/106053 . ISSN   0362-1340.
  13. ↑ Møller, Anders; Schwartzbach, Michael I. (2001-05-01). "The pointer assertion logic engine". Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation. PLDI '01. Snowbird, Utah, USA: Association for Computing Machinery: 221–231. doi:10.1145/378795.378851. ISBN   978-1-58113-414-8. S2CID   11476928.
  14. ↑ Basin, David; Klarlund, Nils (1998-11-01). "Automata based symbolic reasoning in hardware verification". Formal Methods in System Design. 13 (3): 255–288. doi:10.1023/A:1008644009416. ISSN   0925-9856.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.