Content deleted Content added
Replace all "\begin{aligned}" with "\begin{align}" - see talk Talk:Acceleration (special relativity)#Parse error |
m Copyedited |
||
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-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 (distributed computing)|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 is in a class of [[temporal logic]]s that includes [[linear temporal logic]] (LTL). Although there are properties expressible
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.
| |||