Computation tree logic: Difference between revisions

Revision as of 13:20, 7 September 2022

Revision as of 00:55, 29 September 2022

Line 1:

{{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 (distributedand computing)Liveness Properties|safety]] or [[liveness properties]] 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*]].

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.