Monadic second-order logic: Difference between revisions

Revision as of 00:09, 25 August 2022

Latest revision as of 23:48, 19 June 2025

(9 intermediate revisions by 9 users not shown)

Line 1:

{{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-TrakhtenbrotBüchi–Elgot–Trakhtenbrot theorem]] gives a logical characterization of the [[regular language]]s.

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 5 ⟶ 6:

== 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 <math>E(x, y)</math>), but quantification is restricted to be over monadic predicates only. In the variant considered in automata theory and the Büchi-Elgot-TrakhtenbrotBüchi–Elgot–Trakhtenbrot theorem, all predicates, including those in the formula itself, must be monadic, with the exceptions of equality (<math>=</math>) and ordering (<math><</math>) relations.

== Computational complexity of evaluation ==

Line 32 ⟶ 33:

== Decidability and complexity of satisfiability ==

The satisfiability problem for monadic second-order logic is undecidable in general because this logic subsumes [[Firstfirst-order logic]].

The monadic second -order theory of the infinite complete [[binary tree]], called [[S2S (mathematics)|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|url-access=subscription}}</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).

* wS2SWS2S and wS1SWS1S, which restrict quantification to finite subsets (weak monadic second -order logic). Note that for binary numbers (represented by subsets), addition is definable even in wS1SWS1S.

For each of these theories (S2S, S1S, wS2SWS2S, wS1SWS1S), the complexity of the decision problem is [[nonelementary problem|nonelementary]].<ref name=":0" /><ref>{{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>

=== Use of satisfiability of MSO on trees in verification ===

Monadic second-order logic of trees has applications in [[Softwareformal verification]] and, more broadly, [[Formal verification]] thanks to its decidability and significant expressive power. Decision procedures for MSO satisfiability have been implemented.<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> Suchhave procedures werebeen used to prove properties of programs manipulating linked [[data structures]],<ref>{{Cite journalbook|last1=Møller|first1=Anders|last2=Schwartzbach|first2=Michael I.|datetitle=Proceedings of the ACM SIGPLAN 2001-05-01 conference on Programming language design and implementation |titlechapter=The pointer assertion logic engine |date=2001-05-01|chapter-url=https://doi.org/10.1145/378795.378851|journal=Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation|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)|Shapeshape analysis]], as well asand 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>

==See also==

Line 55 ⟶ 56:

{{Mathematical logic}}

{{Logic-stub}}

[[Category:Mathematical logic]]