5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 86
Текст из файла (страница 86)
However, CTL+ formulae can be much shorter than theshortest equivalent CTL formulae.6.8.2CTL∗ Model CheckingThis section treats a model-checking algorithm for CTL∗ . The CTL∗ model-checkingproblem is to establish whether TS |= Φ holds for a given finite transition system TS(without terminal states) and the CTL∗ state formula Φ. As we will see, an appropriatecombination of the model-checking algorithms for LTL and CTL suffices.As for CTL, the model-checking algorithm for CTL∗ is based on a bottom-up traversalof the syntax tree of the formula Φ to be checked. Due to the bottom-up nature of thealgorithm, the satisfaction set Sat(Ψ) for any state sub formulae Ψ of Φ has been computedbefore, and can be used to determine Sat(Φ). This holds in particular for the maximalproper state subformulae of Φ.Definition 6.86.Maximal Proper State SubformulaState formula Ψ is a maximal proper state subformula of Φ whenever Ψ is a subformula ofΦ that differs from Φ and that is not contained in any other proper state subformula ofΦ.The basic concept is to replace all maximal proper state subformulae of Φ by fresh atomicpropositions a1 , .
. . , ak , say. These propositions do not occur in Φ and are such thatai ∈ L(s) if and only if s ∈ Sat(Ψi ), the ith maximal state subformula of Φ. For state428Computation Tree Logicsubformulae whose “top-level” operator is a Boolean operator (such as negation or conjunction), the treatment is obvious. Let us consider the more interesting case of Ψ = ∃ϕ.By replacing all maximal state subformulae in ϕ, an LTL formula results! Sinces |= ∃ϕ iffs | = ∀¬ϕ CTL∗ semanticsiffs | = ¬ϕ , LTL semanticsit suffices to compute the satisfaction setSatLTL (¬ϕ) = { s ∈ S | s |=LTL ¬ϕ }by means of an LTL model checker. (Here, the notations SatLTL (·) and |=LTL are used toemphasize that the basis is the LTL satisfaction relation.) The satisfaction set for Φ = ∃ϕis now obtained by complementation:SatCTL∗ (∃ϕ) = S \ SatLTL (¬ϕ).For CTL∗ formulae where the outermost operator is an universal quantification we simplymay deal withSatCTL∗ (∀ϕ) = SatLTL (ϕ)where, as before, it is assumed that ϕ is an LTL formula resulting from the replacementof the maximal state subformula with fresh atomic propositions.The main steps of the CTL∗ model-checking procedure are presented in Algorithm 27 onpage 429.Example 6.87.Abstract Example of CTL∗ Model CheckingThe CTL∗ model-checking approach is illustrated by considering the CTL∗ formula:∃ϕ where ϕ = (∀ ∃♦ a) ∧ ♦ ∃( a ∧ b).The maximal proper state subformulae of ϕ areΦ1 = ∀ ∃♦ a andΦ2 = ∃( a ∧ b).Thus:ϕ = (∀ ∃♦ a) ∧ ♦ ∃( a ∧ b) = Φ1 ∧ ♦ Φ2 .
Φ1Φ2According to the model-checking algorithm for CTL∗ , the satisfaction sets Sat(Φi ) arecomputed recursively. Subsequently, Φ1 and Φ2 are replaced with the atomic propositionsa1 and a2 , say. This yields the following LTL formula over the set of propositions AP ={ a1 , a2 }:ϕ = a1 ∧ ♦ a2 .CTL∗429Algorithm 27 CTL∗ model checking algorithm (basic idea)Input: finite transition system TS with initial states I, and CTL∗ formula ΦOutput: I ⊆ Sat(Φ)for all i | Φ | dofor all Ψ ∈ Sub(Φ) with | Ψ | = i doswitch(Ψ):trueaa 1 ∧ a2¬a∃ϕ::::::Sat(Ψ) := S;Sat(Ψ) := { s ∈ S | a ∈ L(s) };Sat(Ψ) := Sat(a1 ) ∩ Sat(a2 );Sat(Ψ) := S \ Sat(a);determine SatLTL (¬ϕ) by means of an LTL model-checker;Sat(Ψ) := S \ SatLTL (¬ϕ)end switchAP := AP ∪ { aΨ };replace Ψ with aΨforall s ∈ Sat(Ψ) do L(s) := L(s) ∪ { aΨ }; odododreturn I ⊆ Sat(Φ)(* introduce fresh atomic proposition *)The labeling function L : S → 2AP is given by:ai ∈ L (s) if and only if s ∈ Sat(Φi ) for i ∈ { 1, 2 }.Applying the LTL model-checking algorithm to the formula ¬ϕ yields the set of statessatisfying (with respect to the LTL semantics) ¬ϕ , i.e., SatLTL (¬ϕ ).
The complement ofSatLTL (¬ϕ ) provides the set SatCTL∗ (ϕ).Evidently, the time complexity of the CTL∗ model-checking algorithm is dominated bythe LTL model-checking phases. The additional effort that is necessary for CTL∗ modelchecking is polynomial in the size of the transition system and the length of the formula.Hence, a time complexity is obtained which is exponential in the length of the formulaand linear in the size of the transition system.Theorem 6.88.Time Complexity of CTL∗ Model CheckingFor transition system TS with N states and K transitions, and CTL∗ formula Φ, theCTL∗ model-checking problem TS |= Φ can be determined in time O((N +K)·2|Φ| ).Note that CTL∗ model checking can be solved by any LTL model-checking algorithm.These considerations show that there is a polynomial reduction of the CTL∗ model-430Computation Tree LogicCTLLTLCTL∗model checkingPTIMEPSPACE-completePSPACE-completewithout fairnesssize(TS) · |Φ|size(TS) · exp(|Φ|)size(TS) · exp(|Φ|)with fairnesssize(TS) · |Φ| · |fair |size(TS) · exp(|Φ|) · |fair|size(TS) · exp(|Φ|) · |fair |for fixed specifications(model complexity)size(TS)size(TS)size(TS)satisfiability checkEXPTIMEPSPACE-complete2EXPTIMEbest known techniqueexp(|Φ|)exp(|Φ|)exp(exp(|Φ|))Figure 6.29: Complexity of the model-checking algorithms and satisfiability checking.checking problem to the LTL model-checking problem.
As a result, the theoretical complexity results for LTL also apply to CTL∗ . Table 6.29 summarizes the complexity resultsfor model checking CTL, CTL∗ , and LTL.Theorem 6.89.Theoretical Complexity of CTL∗ Model CheckingThe CTL∗ model-checking problem is PSPACE-complete.6.9Summary• Computation Tree Logic (CTL) is a logic for formalizing properties over computationtrees, i.e., the branching structure of the states.• The expressivenesses of LTL and CTL are incomparable.• Although fairness constraints cannot be encoded in CTL formulae, fairness assumptions can be incorporated in CTL by adapting the CTL semantics such that quantification is over fair paths, rather than over all paths.• The CTL model-checking problem can be solved by a recursive descent procedureover the parse tree of the state formula to be checked.
The set of states satisfying∃(Φ U Ψ) can be determined using a smallest fixed-point procedure; for ∃ Φ this isa largest fixed-point procedure.Bibliographic Notes431• The time complexity of the CTL model-checking algorithm is linear in the size ofthe transition system and the length of the formula. In case fairness constraints areconsidered, an additional multiplicative factor that is proportional to the number offairness constraints needs to be taken into account.• Counterexamples and witnesses for CTL path formulae can be determined using astandard graph analysis.• The CTL model-checking procedure can be realized symbolically by means of orderedbinary decision diagrams.
These provide a universal and canonical data structurefor switching functions.• Extended Computation Tree Logic (CTL∗ ) is more expressive than either CTL andLTL.• The CTL∗ model-checking problem can be solved by an appropriate combination ofthe recursive descent procedure (as for CTL) and the LTL model-checking algorithm.• The CTL∗ model-checking problem is PSPACE-complete.6.10Bibliographic NotesBranching temporal logics. Various types of branching temporal logic have been proposed in the literature. We mention a few important ones in increasing expressive power:Hennessy-Milner logic (HML [197]), Unified System of Branching-Time Logic [42], Computation Tree Logic (CTL [86]), Extended Computation Tree Logic (CTL∗ [86]), and modalμ-Calculus [243].
The modal μ-calculus is the most expressive among these languages,and HML is the least expressive. CTL has been extended with fairness by Emerson andHalpern [140] and by Emerson and Lei [143].Not treated in this textbook is the task of proving satisfiability of formulae by meansof algorithms or deductive techniques. The satisfiability problems for CTL, CTL∗ , andother temporal logics have been addressed by many researchers and used, e.g., in thecontext of synthesis problems where the goal is to design a system model from a giventemporal specification.
Emerson [138] has shown that checking CTL satisfiability is inthe complexity class EXPTIME. This means that the time complexity of checking CTLsatisfiability is exponential in the length of the formula. For CTL∗ this problem is doubleexponential [141] in the length of the formula. A complete axiomatization of CTL hasbeen given by Ben-Ari, Manna and Pnueli [42] and Emerson and Halpern [139].Branching vs. linear temporal logics. The discussion of the relative merits of linear- vs.branching-time logics goes back to the early eighties. Pnueli [338] established that linear432Computation Tree Logicand branching temporal logics are based on two distinct notions of time. Various papers [85, 140, 259] show that the expressivenesses of LTL and CTL are incomparable.
Asomewhat more practical view on comparing the usefulness of LTL vs. CTL was recentlygiven by Vardi [410]. The logic CTL∗ that encompasses LTL and CTL was defined byClarke and Emerson [86].CTL model checking. The first algorithms for CTL model checking were presented byClarke and Emerson [86] in 1981 and (for a logic similar to CTL) by Queille and Sifakis [347]in 1982. The algorithm by Clarke and Emerson was polynomial in both the size of the transition system and the length of the formula, and could handle fairness.
Clarke, Emerson,and Sistla [87] presented an efficiency improvement using the detection of strongly connected components and backward breadth-first search, yielding an algorithm that is linearin both the size of the system and the length of the formula.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
