Computation tree logic

Computation tree logic (CTL) is a branching-time 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 checkers, which determine if a given artifact possesses 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 logics 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 programs. The language of well-formed formulas for CTL is generated by the following grammar: where ranges over a set of atomic formulas. It is not necessary to use all connectives – for example, comprises a complete set of connectives, and the others can be defined using them. means 'along All paths' (inevitably) means 'along at least (there Exists) one path' (possibly) For example, the following is a well-formed CTL formula: The following is not a well-formed CTL formula: The problem with this string is that can occur only when paired with an or an . CTL uses atomic propositions as its building blocks to make statements about the states of a system.