Computation tree logic: Difference between revisions

Revision as of 04:02, 21 June 2024

Latest revision as of 04:16, 23 December 2024

(One intermediate revision by one other user not shown)

Line 1:

{{Short description|Theory in computer science}}

{{More footnotes|date=October 2015}}

'''Computation tree logic''' ('''CTL''') is a branching-time [[Mathematical logic|logic]], meaning that its model of [[time]] is a [[tree (graph theory)|tree-like]] structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in [[formal verification]] of software or hardware artifacts, typically by software applications known as [[model checker]]s, which determine if a given artifact possesses [[Safety and Liveness Properties|safety or liveness properties]]. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of [[temporal logic]]s that includes [[linear temporal logic]] (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in [[CTL*]].

Line 5 ⟶ 6:

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 ⟶ 149:

== 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 ⟶ 163:

==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}}