Computation tree logic: Difference between revisions

Revision as of 10:28, 29 September 2022

Revision as of 13:34, 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 propertyand 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*]].

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.

Line 157:

*[[Fair computational tree logic]]

*[[Linear temporal logic]]

*[[Safety and liveness properties]]

==References==