Computation tree logic: Difference between revisions

Revision as of 03:21, 18 March 2024

Revision as of 03:22, 18 March 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 model checking it is more computationally efficient to model check, CTL has become more common in industrial use, and many of the most successful model-checking tools use CTL as a specification language.<ref>{{cite journal |last1=Vardi |first1=Moshe Y. |date=2001 |title=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 |url=https://link.springer.com/content/pdf/10.1007/3-540-45319-9_1.pdf}}</ref>

== Syntax of CTL ==