Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Computation tree logic
Summary
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.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.