Content deleted Content added
Citation bot (talk | contribs) Alter: template type, title. Add: doi-access, chapter-url, isbn, chapter. Removed or converted URL. Removed parameters. Some additions/deletions were parameter name changes. | Use this bot. Report bugs. | Suggested by Headbomb | Linked from Wikipedia:WikiProject_Academic_Journals/Journals_cited_by_Wikipedia/Sandbox2 | #UCB_webform_linked 378/1051 |
Adding short description: "Theory in computer science" |
||
Line 1:
{{Short description|Theory in computer science}}
{{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 and 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*]].
| |||