A branching temporal logic whose operators quantify over paths in a transition system from a state. In particular, , also written , holds at when every infinite path in a transition system from satisfies at every position, including its initial position.
Articles by others on the same topic
Computation Tree Logic (CTL) is a branching-time temporal logic used for specifying and reasoning about properties of computational processes, particularly in the context of systems that can be modeled as trees of states, such as concurrent systems and reactive systems. It allows for the expression of temporal properties over computation paths, enabling an analysis of how systems behave over time.