Computation tree logic: Difference between revisions

Revision as of 04:02, 21 June 2024

Revision as of 21:34, 28 July 2024

Line 5:

CTL was first proposed by [[Edmund M. Clarke]] and [[E. Allen Emerson]] in 1981, who used it to synthesize so-called ''synchronisation skeletons'', ''i.e'' abstractions of [[concurrent program]]s.

Since the introduction of CTL, there has been debate about the relative merits of CTL and LTL. Because CTL is more computationally efficient to model check, it has become more common in industrial use, and many of the most successful model-checking tools use CTL as a specification language.<ref>{{cite journalbook |last1=Vardi |first1=Moshe Y. |date=2001 |titlechapter=Branching vs. Linear Time: Final Showdown |journal=Tools and Algorithms for the Construction and Analysis of Systems |series=Lecture Notes in Computer Science |volume=2031 | publisher=Springer, Berlin |pages=1{{ndash}}22 |doi=10.1007/3-540-45319-9_1 |isbn=978-3-540-41865-8 |chapter-url=https://link.springer.com/content/pdf/10.1007/3-540-45319-9_1.pdf}}</ref>

== Syntax of CTL ==

Line 148:

== Extensions ==

CTL has been extended with [[second-order logic|second-order]] quantification <math>\exists p</math> and <math>\forall p</math> to ''quantified computational tree logic'' (QCTL).<ref>{{Cite journal|last1=David|first1=Amélie|last2=Laroussinie|first2=Francois|last3=Markey|first3=Nicolas|date=2016|editor-last=Desharnais|editor-first=Josée|editor2-last=Jagadeesan|editor2-first=Radha|title=On the Expressiveness of QCTL|url=http://drops.dagstuhl.de/opus/volltexte/2016/6164|journal=27th International Conference on Concurrency Theory (CONCUR 2016)|series=Leibniz International Proceedings in Informatics (LIPIcs)|___location=Dagstuhl, Germany|publisher=Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik|volume=59|pages=28:1–28:15|doi=10.4230/LIPIcs.CONCUR.2016.28|doi-access=free |isbn=978-3-95977-017-0}}</ref> There are two semantics:

* the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = [[monadic second-order logic|MSO]] over trees. Model checking and satisfiability are tower complete.

* the structure semantics. We label states. QCTL* = QCTL = MSO over [[Graph (discrete mathematics)|graph]]s. Model checking is [[PSPACE-complete]] but satisfiability is [[undecidable problem|undecidable]].

A reduction from the model-checking problem of QCTL with the structure semantics, to TQBF (true quantified Boolean formulae) has been proposed, in order to take advantage of the QBF solvers.<ref>{{Cite journal|last1=Hossain|first1=Akash|last2=Laroussinie|first2=François|date=2019|editor-last=Gamper|editor-first=Johann|editor2-last=Pinchinat|editor2-first=Sophie|editor3-last=Sciavicco|editor3-first=Guido|title=From Quantified CTL to QBF|url=http://drops.dagstuhl.de/opus/volltexte/2019/11369|journal=26th International Symposium on Temporal Representation and Reasoning (TIME 2019)|series=Leibniz International Proceedings in Informatics (LIPIcs)|___location=Dagstuhl, Germany|publisher=Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik|volume=147|pages=11:1–11:20|doi=10.4230/LIPIcs.TIME.2019.11|doi-access=free |isbn=978-3-95977-127-6|s2cid=195345645 }}</ref>

==See also==

Line 162:

==References==

{{Reflist}}

* {{cite journalbook |author1=E.M. Clarke |author2=E.A. Emerson | titlechapter=Design and synthesis of synchronisation skeletons using branching time temporal logic| journaltitle=Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science |series=Lecture Notes in Computer Science |volume=131 | publisher= Springer, Berlin | year=1981 |pages= 52–71|doi=10.1007/BFb0025774 |isbn=3-540-11212-X |chapter-url=https://www.cs.cmu.edu/afs/cs/user/emc/www/papers/Invited%20Conference%20Articles/Design%20and%20Synthesis%20of%20Synchronization%20Skeletons%20Using%20Branching%20Time%20Temporal%20Logic.pdf}}

* {{cite book |author1=Michael Huth |author2=Mark Ryan | title=Logic in Computer Science | year=2004| page=207 | publisher=Cambridge University Press | isbn=978-0-521-54310-1|edition=Second }}

* {{cite journal |author1=Emerson, E. A. |author2=Halpern, J. Y. |author2link = Joseph Halpern| title=Decision procedures and expressiveness in the temporal logic of branching time | journal=[[Journal of Computer and System Sciences]]| year=1985| volume=30 | issue=1 | pages=1–24 | doi=10.1016/0022-0000(85)90001-7| citeseerx=10.1.1.221.6187}}