Monadic second-order logic: Difference between revisions

Revision as of 16:45, 18 April 2025

Latest revision as of 23:48, 19 June 2025

Line 35:

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

* 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|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 [[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 (program analysis)|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>

==See also==