Concept

CTL*

Overview

CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.

Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).

Related ideas

• Formal language
• Propositional logic
• Formal verification
• Model checking
• Temporal logic
• Association for Symbolic Logic
• Atomic formula
• Context-free grammar
• Linear temporal logic
• Computational complexity theory
• Computation tree logic

Place in the tradition

Part of Temporal logic.

Explore CTL* in the interactive graph →