Content deleted Content added
m →References: task, replaced: journal=Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, Vol. → journal=Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science |vol |
No edit summary |
||
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 (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
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 92:
===Semantic equivalences===
The formulae <math>\phi</math> and <math>\psi</math> are said to be semantically equivalent if any state in any model
This is denoted <math>\phi \equiv \psi</math>
| |||