Computation tree logic
Computation tree logic (CTL) is a propositional branching-time temporal logic that extends propositional logic with temporal operators to specify and verify properties of concurrent systems modeled as state-transition graphs, where time is represented as a tree of possible computations branching into multiple futures.[1] Introduced by Edmund M. Clarke and E. Allen Emerson in 1981, CTL enables the expression of both universal (inevitable) and existential (possible) behaviors over these branching structures, distinguishing it from linear-time logics like LTL that consider only single execution paths.[1][2] CTL's syntax includes atomic propositions from a set AP, boolean connectives (¬, ∧, ∨), and modal operators combining path quantifiers—A (for all paths) and E (there exists a path)—with temporal operators such as X (next state), F (eventually), G (always), and U (until).[3] For example, the formula AF p asserts that on all paths from the current state, proposition p will eventually hold, while EF p states that there exists at least one path where p eventually holds.[2] Semantics are defined over Kripke structures M = (S, R, L), where S is a finite set of states, R ⊆ S × S the transition relation, and L: S → 2^{AP} labels states with propositions; a structure satisfies a CTL formula if the initial state meets the formula's conditions along its computation tree.[3] The logic's significance lies in its role in model checking, an automated verification technique where a system's state space is exhaustively explored to confirm if it satisfies CTL specifications, with algorithms achieving linear time complexity in the model size and formula length—specifically O(|f| · (|S| + |R|)) for a formula f and structure with |S| states and |R| transitions.[4] This efficiency, first demonstrated in Clarke, Emerson, and Sistla's 1983 work (extended to journal in 1986), made CTL practical for verifying hardware circuits, communication protocols, and software systems, contributing to the 2007 Turing Award for Clarke, Emerson, and Joseph Sifakis for pioneering model checking.[4][2] CTL has influenced extensions like CTL* (combining branching and linear aspects) and tools such as NuSMV, which support industrial-scale verification by generating counterexamples for debugging when properties fail.[5]Introduction
Overview and Definition
Computation Tree Logic (CTL) is a propositional branching-time temporal logic designed to specify and reason about properties of reactive and concurrent systems. It enables the expression of behaviors over possible execution paths in non-deterministic environments, distinguishing it from linear-time logics by accounting for branching structures in system computations.[1] In CTL, computation trees represent the unfolding of all possible execution paths originating from an initial state, where each node corresponds to a system state and branches reflect non-deterministic choices or interleavings of concurrent processes. This tree structure captures the full spectrum of potential system evolutions, allowing properties to be asserted about entire sets of paths rather than single traces.[1] The name "Computation Tree Logic" reflects its foundational reliance on these computation trees to model non-deterministic behaviors in concurrent systems, as introduced in the seminal work by Clarke and Emerson. At its core, CTL formulas combine path quantifiers—such as A (for all paths) and E (for some path)—with temporal modalities, including X (next state), F (eventually), G (globally), and U (until), to describe universal or existential properties along branches.[1]Role in Formal Verification
Computation tree logic (CTL) plays a central role in formal verification by enabling the specification of safety and liveness properties for both hardware and software systems modeled as finite-state transition systems.[6] Safety properties, such as mutual exclusion in concurrent processes, can be expressed using the universally quantified always operator (AG), ensuring that undesirable states are never reached along any computation path.[6] Liveness properties, like eventual response in reactive systems, are captured with operators such as AF (always eventually), guaranteeing progress toward desired outcomes in all possible futures.[6] This makes CTL particularly suited for verifying systems where nondeterminism leads to branching behaviors, such as in concurrent protocols or embedded controllers.[7] One key advantage of CTL in formal verification is its expressive power for describing branching-time properties, which naturally models the multiple possible execution paths in nondeterministic systems, unlike linear-time logics that assume a single path.[7] Model checking for CTL formulas against finite-state models is decidable and can be performed in time linear in the size of the model (number of states and transitions) and the formula, specifically O(|Φ| · (|S| + |R|)), where |Φ| is the formula size, |S| the number of states, and |R| the number of transitions.[8] This polynomial-time complexity supports scalable automated verification, often producing counterexamples or witnessing paths to aid debugging when properties fail.[6] CTL integrates seamlessly with symbolic model checking tools such as SMV and its successor NuSMV, which use binary decision diagrams (BDDs) to handle large state spaces efficiently for verifying concurrent systems.[9] These tools automate the checking of CTL specifications on hardware designs, enabling exhaustive exploration without simulation.[10] In practice, CTL has significantly impacted hardware design by verifying circuit behaviors, protocol verification through properties like deadlock freedom in cache coherence protocols, and reactive systems engineering, where it ensures reliability in safety-critical applications such as fault-tolerant voting systems.[6] Its adoption contributed to the 2007 ACM Turing Award for advancing model checking techniques.[6] Despite these strengths, CTL has limitations as a specification language, particularly for linear-time properties that unfold along a single execution trace, where it is less intuitive and expressive compared to linear temporal logic (LTL), as CTL requires path quantifiers that can complicate simple sequential assertions.[7] This can lead to more verbose or less natural formulations for properties like response times in sequential protocols, often favoring LTL or extensions like CTL* for such cases.[7]Historical Development
Origins in Temporal Logic
Computation tree logic (CTL) traces its origins to the development of temporal logics in the late 1970s, which sought to formalize properties of computer programs over time. In 1977, Amir Pnueli introduced linear temporal logic (LTL) as a tool for specifying and verifying the behavior of non-terminating programs, particularly reactive systems that engage in infinite computations.[11] Pnueli's framework emphasized ongoing behaviors rather than finite input-output relations, using operators to express temporal relations such as "always" and "eventually" along a single execution path.[12] This innovation marked a foundational shift in program verification, enabling the description of safety and liveness properties in concurrent settings.[13] However, LTL's linear-time semantics, which assumes a single, deterministic sequence of states, proved limiting for modeling non-deterministic concurrent programs where multiple execution paths branch from choice points.[12] Such systems, common in parallel computing, generate tree-like structures of possible computations, reflecting the inherent uncertainty of future states due to non-determinism.[13] Early motivations for extending temporal logic thus centered on capturing these branching possibilities to verify properties across all or some potential paths in infinite computations.[12] To address these shortcomings, researchers began exploring branching-time temporal logics in the early 1980s, with Pnueli's LTL serving as a key precursor that highlighted the need for path quantifiers to distinguish universal and existential claims over tree-structured models.[13] This evolution paved the way for logics like CTL, which incorporated quantifiers over paths to explicitly handle the non-deterministic, tree-like nature of computations in concurrent programs.Key Milestones and Contributors
Computation Tree Logic (CTL) was first introduced in 1981 by Edmund M. Clarke and E. Allen Emerson in their seminal paper "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic," where they proposed CTL as a branching-time temporal logic for specifying and synthesizing synchronization properties in concurrent systems. In 1986, Clarke, Emerson, and A. Prasad Sistla expanded on this foundation in "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," developing an efficient model-checking algorithm for CTL and proving that the problem is P-complete, which established CTL as a cornerstone for automatic verification of finite-state systems.[4] Key contributors to CTL's development include Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis, whose pioneering work on model checking—encompassing CTL's theoretical and practical advancements—earned them the 2007 ACM A.M. Turing Award for transforming model checking into a widely adopted verification technology.[14] During the 1990s, Kenneth L. McMillan advanced CTL through the integration of symbolic model checking using Binary Decision Diagrams (BDDs), as detailed in his 1990 paper "Symbolic Model Checking: 10^20 States and Beyond" (co-authored with Jerry R. Burch and David L. Dill), which enabled efficient verification of systems with enormous state spaces by representing transition relations symbolically rather than explicitly.[15] Post-2000 developments have extended CTL to handle probabilistic and real-time aspects, with Probabilistic CTL (PCTL) seeing algorithmic improvements for model checking Markov decision processes, as in the 2003 survey "Model Checking for Probability and Time: From Theory to Practice," which bridged CTL's branching structure with probabilistic quantification for stochastic systems.[16] Similarly, Timed CTL (TCTL) has been extended with strategic operators in works like the 2023 paper "Strategic Timed Computation Tree Logic," incorporating game-theoretic elements for verifying real-time systems under adversarial conditions. More recent advances include robust CTL (rCTL) in 2024, which introduces multi-valued semantics to quantify specification violations for enhanced verification robustness.[17] As of 2025, CTL remains relevant in formal verification and AI applications, such as inferring temporal properties from system models and providing explainability for AI planning techniques like Monte Carlo Tree Search (MCTS), as demonstrated in the 2023 study "Inferring Properties in Computation Tree Logic," which develops counterexample-guided algorithms to automatically generate concise CTL specifications from finite-state models,[18] and 2024-2025 works on CTL-based explainers for MCTS in sequential planning.[19][20]Syntax
Formula Construction
Atomic propositions serve as the foundational elements in the construction of Computation Tree Logic (CTL) formulas, where each atomic proposition p from a finite set AP of atomic propositions denotes a basic state label indicating the presence or absence of a specific property in a model state.[4] CTL formulas are built recursively, distinguishing between state formulas, which are interpreted over individual states, and path formulas, which are interpreted over infinite paths emanating from those states. State formulas are formed starting from atomic propositions and applying boolean negation (\neg), conjunction (\land), and the path quantifiers A (universal, "for all paths") and E (existential, "there exists a path") to path formulas. Path formulas are constructed from state formulas using the next operator X (applied to a state formula) and the until operator U (between two state formulas). Disjunction (\lor) and other boolean connectives such as implication (\rightarrow) and equivalence (\leftrightarrow) can be derived from negation and conjunction using standard logical equivalences. This recursive structure ensures that every temporal operator in CTL is immediately preceded by a path quantifier, enforcing the logic's branching-time nature. CTL formulas are typically closed, meaning they contain no free variables and thus evaluate to true or false with respect to a model without additional bindings. State formulas represent properties of states and serve as the primary specifications in CTL, while path formulas act as intermediates scoped by the quantifiers A and E. The absence of free variables in atomic propositions propagates through the recursive construction, yielding well-formed, interpretable formulas suitable for formal verification.[4] The syntax of CTL is formally defined by the following context-free grammar in Backus-Naur Form (BNF), where p \in AP:This grammar captures the core operators, with derived forms such as eventually (F \phi \equiv \top U \phi), always (G \phi \equiv \neg (\top U \neg \phi)), and their universal/existential variants expressible through these primitives.state formula φ ::= p | ¬φ | φ₁ ∧ φ₂ | A ψ | E ψ path formula ψ ::= φ | X φ | φ₁ U φ₂state formula φ ::= p | ¬φ | φ₁ ∧ φ₂ | A ψ | E ψ path formula ψ ::= φ | X φ | φ₁ U φ₂
Operators and Quantifiers
Computation tree logic (CTL) employs a set of operators that combine path quantifiers with temporal modalities and classical logical connectives to form well-structured formulas. These operators enable the expression of properties over branching computation paths in transition systems. The syntax distinguishes between state formulas, which are evaluated at individual states, and path formulas, which describe properties along paths emanating from a state. The path quantifiers are A and E, which are unary operators applied to path formulas. The quantifier A asserts that a property holds for all computation paths starting from the current state, while E asserts that there exists at least one such path where the property holds. These quantifiers bind path formulas to form state formulas, ensuring that temporal modalities are always scoped by a path quantifier in CTL syntax. Temporal operators in CTL include both primitive and derived forms, all of which operate on state subformulas. The primitive unary operator X (next) applies to a state formula to specify a property in the immediate successor state along a path. The primitive binary operator U (until) takes two state formulas \phi and \psi, expressing that \phi holds along a path until \psi becomes true. Derived unary temporal operators include F (eventually), defined syntactically as \top U \phi where \top is the constant true, and G (globally), defined as \neg F \neg \phi. The derived binary operator R (release), the dual of until, is defined as \neg (\neg \phi U \neg \psi). These temporal operators form path formulas when combined appropriately, such as \phi U \psi, which must then be quantified by A or E to yield a state formula. Logical operators provide the boolean structure for CTL formulas and include the unary negation \neg and the binary conjunction \wedge and disjunction \vee. Derived binary operators include implication \rightarrow, defined as \neg \phi \vee \psi, and equivalence \leftrightarrow, defined as (\phi \rightarrow \psi) \wedge (\psi \rightarrow \phi). Atomic propositions and the constants \top and \bot serve as base state formulas. These operators apply to state formulas to build more complex ones. Operator binding in CTL enforces that path quantifiers immediately precede temporal operators, as in the state formula AGp, where A binds to the unary G applied to the atomic proposition p. In contrast, p U q is a path formula requiring quantification, such as E(p U q), to form a state formula. This binding rule prevents ambiguous nesting and maintains the alternation between path quantifiers and temporal modalities. Unary operators like X, G, F, and \neg take a single operand, while binary operators such as U, R, \wedge, and \vee take two.Minimal Operator Sets
In Computation Tree Logic (CTL), a minimal operator set consists of the path quantifiers E (exists) and A (for all), along with the temporal operators X (next) and U (until), which, together with standard Boolean connectives, form a complete basis capable of expressing all CTL formulas. This set is sufficient because the universal quantifier A can be derived from the existential E via duality (A \phi \equiv \neg E \neg \phi), allowing an even more compact basis of \{E, X, U\} with negation. To demonstrate completeness, other common temporal operators can be derived from these primitives. For instance, the eventually operator F \phi is defined as E(\top U \phi), where \top denotes true; the always operator G \phi follows as \neg E F \neg \phi or equivalently A(\neg \phi R \bot); and the release operator \phi R \psi is \neg E(\neg \phi U \neg \psi). These equivalences ensure that operators like AF, EG, and AX—frequently used in specifications—can be reduced to the core set without loss of expressiveness. Alternative minimal bases exist, such as \{E, X, U, \neg\}, which explicitly includes negation to handle duals, or sets relying solely on existential operators with derived universals.[21] Another variant is \{\neg, \lor, EX, EU, EG\}, where EG (exists globally) aids in expressing infinite path properties directly.[22] The identification of these minimal sets traces back to the foundational development of CTL, where efficiency in specification and verification was a key concern from the outset.[1] In practice, adopting a minimal basis simplifies the implementation of model checkers by reducing the number of semantic rules and fixed-point computations needed, thereby lowering computational overhead in tools like NuSMV or SPIN.Semantics
Kripke Structures and Models
In computation tree logic (CTL), the semantic models are provided by Kripke structures, which represent the state space of concurrent systems as labeled transition systems. A Kripke structure over a set AP of atomic propositions is defined as a tuple M = (S, S_0, R, L), where S is a finite, nonempty set of states; S_0 \subseteq S is a nonempty set of designated initial states; R \subseteq S \times S is a transition relation that is total, meaning every state has at least one successor (i.e., \forall s \in S: \exists s' \in S such that (s, s') \in R); and L: S \to 2^{AP} is a labeling function that assigns to each state the set of atomic propositions that hold in it.[23] This structure captures the branching nature of computations in nondeterministic systems, where multiple possible futures arise from each state. The computations in a Kripke structure are represented by paths, which are infinite sequences of states. Formally, a path \pi of M is an infinite sequence \pi = s_0 s_1 s_2 \dots such that s_0 \in S_0 and (s_i, s_{i+1}) \in R for all i \geq 0.[23] Finite paths are the initial segments of such infinite paths, serving as prefixes up to some length k \geq 0.[23] Paths may include "stutters," where consecutive states are identical (s_i = s_{i+1}), reflecting possible idle or repeated behaviors in the system; however, stutter-free paths, which prohibit such repetitions, are sometimes considered in analyses to simplify equivalence checks without altering the expressive power of CTL.[23] To emphasize the branching-time aspect of CTL, the Kripke structure can be unfolded into computation trees starting from the initial states. A computation tree for M from an initial state s_0 \in S_0 is the infinite tree obtained by iteratively expanding successors according to R, where the root is s_0 and each node at depth i branches to the possible next states, labeled by L. Each infinite path in this tree corresponds to a full computation path in M, providing a tree-like model of all possible execution traces from s_0. This unfolding abstracts away cycles in the structure, focusing on the tree of futures as the basis for evaluating branching-time properties.[23]Satisfaction and Evaluation
The satisfaction of a Computation Tree Logic (CTL) formula is defined with respect to a Kripke structure M and either a state s in M or a path \pi in M. The relation M, s \models \phi holds if state s satisfies the state formula \phi in M, while M, \pi \models \psi holds if path \pi satisfies the path subformula \psi in M.[24][25] The satisfaction relation for state formulas is defined inductively as follows. For an atomic proposition p, M, s \models p if and only if p \in L(s), where L(s) is the set of atomic propositions labeling state s. For negation, M, s \models \neg \phi if and only if M, s \not\models \phi. For conjunction, M, s \models \phi \wedge \psi if and only if M, s \models \phi and M, s \models \psi. For the universal next operator, M, s \models AX \phi if and only if for every successor state s' such that (s, s') \in R, it holds that M, s' \models \phi, where R is the transition relation of M. For the existential next operator, M, s \models EX \phi if and only if there exists a successor state s' such that (s, s') \in R and M, s' \models \phi. For the universal until operator, M, s \models \phi \, AU \, \psi if and only if every infinite path \pi starting from s satisfies M, \pi \models \phi \, U \, \psi. For the existential until operator, M, s \models \phi \, EU \, \psi if and only if there exists an infinite path \pi starting from s such that M, \pi \models \phi \, U \, \psi.[24][25] Path satisfaction is defined for the temporal operators underlying the path quantifiers. Let \pi = \pi{{grok:render&&&type=render_inline_citation&&&citation_id=0&&&citation_type=wikipedia}}, \pi{{grok:render&&&type=render_inline_citation&&&citation_id=1&&&citation_type=wikipedia}}, \pi{{grok:render&&&type=render_inline_citation&&&citation_id=2&&&citation_type=wikipedia}}, \dots be an infinite path with \pi{{grok:render&&&type=render_inline_citation&&&citation_id=0&&&citation_type=wikipedia}} = s. Then M, \pi \models X \phi if and only if M, \pi{{grok:render&&&type=render_inline_citation&&&citation_id=1&&&citation_type=wikipedia}} \models \phi. For the until operator, M, \pi \models \phi \, U \, \psi if and only if there exists some k \geq 0 such that M, \pi \models \psi and for all $0 \leq i < k, M, \pi \models \phi.[24][25] A Kripke structure M satisfies a state formula \phi, written M \models \phi, if and only if M, s \models \phi for every initial state s \in S_0, where S_0 is the set of initial states in M. This ensures that the property expressed by \phi holds from all possible starting points of the system.[24][25]Semantic Equivalences
In Computation Tree Logic (CTL), semantic equivalences arise from the interplay between path quantifiers (A for "all paths" and E for "exists path") and temporal operators, enabling formula simplifications and transformations while preserving satisfaction in Kripke structures. These equivalences are fundamental for reducing the complexity of model checking and optimizing formula representations.[4] Key dualities express negations of universal path formulas in terms of existential ones and vice versa, leveraging De Morgan-like laws adapted to branching-time semantics:- \neg A \psi \equiv E \neg \psi
- \neg EX \phi \equiv AX \neg \phi
- \neg AF \phi \equiv AG \neg \phi
- \neg A(\phi \, U \, \psi) \equiv E(\neg \psi \, R \, \neg \phi)
- F \phi \equiv E(\top \, U \, \phi) (eventually \phi on some path)
- G \phi \equiv \neg E F \neg \phi (always \phi on all paths)
- A(\phi \, R \, \psi) \equiv \neg E(\neg \phi \, U \, \neg \psi) (release: \phi holds on all paths until \psi releases it)
Model Checking
Algorithms for CTL
Model checking for Computation Tree Logic (CTL) involves verifying whether a given Kripke structure satisfies a CTL formula by computing the set of states that satisfy each subformula. The foundational algorithm, introduced by Clarke, Emerson, and Sistla, employs a bottom-up labelled subgraph approach, where satisfying states for atomic propositions are initially identified, and then iteratively computed for increasingly complex subformulas until the entire formula is evaluated.[26] This method leverages the tree-like structure of CTL paths, propagating satisfaction labels through the state graph in a single pass over the formula's syntax tree. CTL operators are characterized using fixed-point equations, enabling efficient computation of satisfying state sets. For instance, the universal "always" operator AGφ, meaning φ holds globally on all paths from a state, is the greatest fixed point of the monotonic function λZ. (φ ∧ AX Z), where AX Z denotes states whose all successors satisfy Z.[26] Similarly, the existential "sometimes" operator EFφ, indicating a path exists where φ eventually holds, is the least fixed point of λZ. (φ ∨ EX Z), with EX Z representing states with at least one successor in Z.[26] These characterizations exploit the μ-calculus foundations of CTL, allowing iterative approximation: starting from the full state set for greatest fixed points and the empty set for least fixed points, refining until convergence.[26] Recursive procedures handle basic operators directly. For the universal next AXφ, satisfaction is checked by verifying that all successor states satisfy φ, computed via a simple graph traversal.[26] The existential until EU(ψ, φ), requiring a path where ψ holds until φ, uses an iterative breadth-first search starting from states satisfying φ, expanding backwards through states satisfying ψ until the fixed point is reached, akin to reachability computation in the graph.[26] Boolean connectives and path quantifiers are then combined recursively from these base cases. To address the state explosion problem in large Kripke structures, symbolic implementations represent sets of states and transition relations implicitly using Binary Decision Diagrams (BDDs).[15] Pioneered by Burch, Clarke, and McMillan, this approach replaces explicit enumeration with BDD operations for fixed-point iterations, such as image computations for EX and predecessor computations for AX, enabling verification of systems with over 10^20 states.[15] BDDs maintain canonical representations, allowing efficient manipulation via Boolean algebra without storing individual states. These algorithms are sound and complete with respect to CTL semantics, as the fixed-point computations precisely capture the inductive definitions of satisfaction in Kripke structures.[26] Termination is guaranteed for finite-state models, since the state space is finite and fixed-point iterations are monotonic, converging in at most |S| + 1 steps where |S| is the number of states.[26]Computational Complexity
The model checking problem for computation tree logic (CTL) over finite Kripke structures is P-complete. This means it is solvable in polynomial time, but no faster deterministic algorithm is known unless P = NC. The combined complexity, considering both the model size (|S| + |R|, where |S| is the number of states and |R| the number of transitions) and formula size (|\phi|), is O((|S| + |R|) \cdot |\phi|).[27] For specific CTL operators, complexities vary based on the labeling algorithm's fixpoint computations. The next-time operators AX (all paths) and EX (exists path) require O(|R|) time, as they involve a single pass over the transition relation to compute predecessor states. Path quantifiers with unary temporal operators, such as AF (all paths eventually), AG (all paths always), EF (exists path eventually), and EG (exists path always), run in O(|S| + |R|) time using breadth-first or depth-first search-like iterations for fixpoint approximation. The until operators AU (all paths until) and EU (exists path until) also require O(|S| + |R|) time, using iterative fixed-point computations equivalent to reachability analysis in the graph.[8] Space complexity for CTL model checking is O(|S|) in on-the-fly algorithms that label states incrementally without storing the full computation table, making it efficient for explicit-state representations. However, the state explosion problem—where |S| grows exponentially with the input program size—leads to exponential space and time in practice for concurrent systems. Optimizations mitigate this: partial order reduction prunes independent transitions to explore fewer states, often reducing effective |S| by orders of magnitude in asynchronous models; symmetry exploitation identifies equivalent states under permutations, further compressing the state space; and symbolic methods using binary decision diagrams (BDDs) represent sets implicitly, achieving polynomial time and space for many scalable verification tasks.[8] Inherent limitations arise in extensions: CTL* model checking is PSPACE-complete, as it combines branching and linear aspects requiring exponential space for path exploration. In comparison, linear temporal logic (LTL) model checking is also PSPACE-complete, highlighting CTL's relative efficiency for branching-time properties.Examples and Applications
Illustrative Examples
To illustrate the syntax and semantics of Computation Tree Logic (CTL), consider simple examples using small Kripke structures. These examples demonstrate how path quantifiers (A for all paths, E for some path) combine with temporal operators to express safety and liveness properties in concurrent systems. Each example includes a basic Kripke structure with 3-5 states, labeled by atomic propositions, and traces satisfying paths to clarify evaluation. Example 1: AG p for mutual exclusion in a two-process system.Consider a simple two-process mutual exclusion protocol modeled as a Kripke structure with four states:
- s_0: initial state (no process in critical section, labeled \neg cs_1 \land \neg cs_2).
- s_1: process 1 in critical section (cs_1 \land \neg cs_2).
- s_2: process 2 in critical section (\neg cs_1 \land cs_2).
- s_3: both attempting entry but serialized (\neg cs_1 \land \neg cs_2, transient).
For a request-grant protocol, model the system with three states:
- s_0: idle (labeled \neg \text{request} \land \neg \text{grant}).
- s_1: request issued (\text{request} \land \neg \text{grant}).
- s_2: grant acknowledged (\neg \text{request} \land \text{grant}).
In a resource allocation system, use a Kripke structure with three states:
- s_0: safe allocation (p \land \neg q).
- s_1: continued safe use (p \land \neg q).
- s_2: release or error (\neg p \land q).