5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 64
Текст из файла (страница 64)
The foundations of this algorithm are discussed and the adaptationsneeded to incorporate fairness are detailed. This is followed by an algorithm for thegeneration of counterexamples. The chapter is concluded by presenting a model-checkingalgorithm for CTL∗ , a branching-time logic that subsumes both LTL and CTL.6.1IntroductionPnueli [337] has introduced linear temporal logic for the specification and verification ofreactive systems. LTL is called linear, because the qualitative notion of time is path-basedand viewed to be linear: at each moment of time there is only one possible successor stateand thus each time moment has a unique possible future.
Technically speaking, this followsfrom the fact that the interpretation of LTL formulae is defined in terms of paths, i.e.,sequences of states.Paths themselves, though, are obtained from a transition system that might be branching:a state may have several, distinct direct successor states, and thus several computationsmay start in a state. The interpretation of LTL-formulae in a state requires that a formulaϕ holds in state s if all possible computations that start in s satisfy ϕ. The universal313314Computation Tree Logicquantification over all computations that is implicit in the LTL semantics can also bemade explicit in the formula, e.g.:s |= ∀ϕ if and only if π |= ϕ for all paths π starting in sIn LTL, we thus can state properties over all possible computations that start in a state,but not easily about some of such computations.
To some extent this may be overcomeby exploiting the duality between universal and existential quantification. For instance, tocheck whether there exists some computation starting in s that satisfies ϕ we may checkwhether s |= ∀ ¬ ϕ; if this formula is not satisfied by s, then there must be a computationthat meets ϕ, otherwise they should all refute ϕ.For more complicated properties, like “for every computation it is always possible to returnto the initial state”, this is, however, not possible. A naive attempt would be to require ♦ start for every computation, i.e., s |= ∀ ♦ start, where the proposition start uniquelyidentifies the initial state. This is, however, too strong as it requires a computation toalways return to the initial state, not just possibly.
Other attempts to specify the intendedproperty also fail, and it even turns out to be the case that the property cannot be specifiedin LTL.To overcome these problems, in the early eighties another strand of temporal logics forspecification and verification purposes was introduced by Clarke and Emerson [86]. Thesemantics of this kind of temporal logic is not based on a linear notion of time—an infinitesequence of states—but on a branching notion of time—an infinite tree of states. Branchingtime refers to the fact that at each moment there may be several different possible futures.Each moment of time may thus split into several possible futures.
Due to this branchingnotion of time, this class of temporal logic is known as branching temporal logic. Thesemantics of a branching temporal logic is defined in terms of an infinite, directed treeof states rather than an infinite sequence. Each traversal of the tree starting in its rootrepresents a single path. The tree itself thus represents all possible paths, and is directlyobtained from a transition system by “unfolding” at the state of interest. The tree rootedat state s thus represents all possible infinite computations in the transition system thatstart in s.
Figure 6.1 depicts a transition system and its unfolding. (For convenience, eachnode in the tree consists of a pair indicating the state and the level of the node in thetree.)The temporal operators in branching temporal logic allow the expression of properties ofsome or all computations that start in a state.
To that end, it supports an existentialpath quantifier (denoted ∃) and a universal path quantifier (denoted ∀). For instance, theproperty ∃♦ Φ denotes that there exists a computation along which ♦ Φ holds. That is,it states that there is at least one possible computation in which a state that satisfies ΦIntroduction315(s0 , 0)(s1 , 1)s1 { x = 0 }s0{ x = 0 }(s2 , 2)s2 { x = 0 }s3{ x = 1, x = 0 }(a)(s3 , 3)(s2 , 4)(s3 , 2)(s2 , 3)(s3 , 3)(s3 , 4) (s3 , 4)(s2 , 4)(s3 , 4)(b)Figure 6.1: (a) A transition system and (b) a prefix of its infinite computation treeis eventually reached. This does not, however, exclude the fact that there can also becomputations for which this property does not hold, for instance, computations for whichΦ is always refuted. The property ∀♦ Φ, in contrast, states that all computations satisfythe property ♦ Φ.
More complicated properties can be expressed by nesting universaland existential path quantifiers. For instance, the aforementioned property “for everycomputation it is always possible to return to the initial state” can be faithfully expressedby ∀ ∃♦ start: in any state () of any possible computation (∀), there is a possibility (∃)to eventually return to the start state (♦ start).This chapter considers Computation Tree Logic (CTL), a temporal logic based on propositional logic with a discrete notion of time, and only future modalities. CTL is an importantbranching temporal logic that is sufficiently expressive for the formulation of an important set of system properties.
It was originally used by Clarke and Emerson [86] and (ina slightly different form) by Queille and Sifakis [347] for model checking. More importantly, it is a logic for which efficient and—as we will see—rather simple model-checkingalgorithms do exist.Anticipatory to the results presented in this chapter, we summarize the major aspects ofthe linear-vs-branching-time debate and provide arguments that justify the treatment ofmodel checking based on linear or branching time logics:• The expressiveness of many linear and branching temporal logics is incomparable.This means that some properties that are expressible in a linear temporal logiccannot be expressed in certain branching temporal logics, and vice versa.316Computation Tree LogicAspectLinear timeBranching time“behavior”in a state spath-based:trace(s)state-based:computation tree of stemporallogicLTL: path formulae ϕs |= ϕ iff∀π ∈ Paths(s).
π |= ϕCTL: state formulaeexistential path quantification ∃ϕuniversal path quantification: ∀ϕcomplexity of themodel checkingproblemsPSPACE–completePTIMEO (|TS| · exp(|ϕ|))O(|TS| · |Φ|)implementationrelationtrace inclusion and the like(proof is PSPACE-complete)simulation and bisimulation(proof in polynomial time)fairnessno special techniques neededspecial techniques neededTable 6.1: Linear-time vs.
branching-time in a nutshell.• The model-checking algorithms for linear and branching temporal logics are quitedifferent. This results, for instance, in significantly different time and space complexity results.• The notion of fairness can be treated in linear temporal logic without the need forany additional machinery since fairness assumptions can be expressed in the logic.For various branching temporal logics this is not the case.• The equivalences and preorders between transition systems that “correspond” tolinear temporal logic are based on traces, i.e., trace inclusion and equality, whereasfor branching temporal logic such relations are based on simulation and bisimulationrelations (see Chapter 7).Table 6.1 summarizes the main differences between the linear-time and branching-timeperspective in a succinct way.Computation Tree Logic6.2317Computation Tree LogicThis section presents the syntax and the semantics of CTL.
The following sections willdiscuss the relation and differences between CTL and LTL, present a model-checkingalgorithm for CTL, and introduce some extensions of CTL.6.2.1SyntaxCTL has a two-stage syntax where formulae in CTL are classified into state and pathformulae. The former are assertions about the atomic propositions in the states and theirbranching structure, while path formulae express temporal properties of paths. Comparedto LTL formulae, path formulae in CTL are simpler: as in LTL they are built by thenext-step and until operators, but they must not be combined with Boolean connectivesand no nesting of temporal modalities is allowed.Definition 6.1.Syntax of CTLCTL state formulae over the set AP of atomic proposition are formed according to thefollowing grammar:Φ ::= trueaΦ1 ∧ Φ2¬Φ∃ϕ∀ϕwhere a ∈ AP and ϕ is a path formula.
CTL path formulae are formed according to thefollowing grammar:ϕ ::= ΦΦ1 U Φ2where Φ, Φ1 and Φ2 are state formulae.Greek capital letters will denote CTL state formulae (CTL formulae, for short), whereaslowercase Greek letters will denote CTL path formulae.CTL distinguishes between state formulae and path formulae. Intuitively, state formulaeexpress a property of a state, while path formulae express a property of a path, i.e., aninfinite sequence of states. The temporal operators and U have the same meaning asin LTL and are path operators.
Formula Φ holds for a path if Φ holds at the nextstate in the path, and Φ U Ψ holds for a path if there is some state along the path forwhich Ψ holds, and Φ holds in all states prior to that state. Path formulae can be turnedinto state formulae by prefixing them with either the path quantifier ∃ (pronounced “forsome path”) or the path quantifier ∀ (pronounced “for all paths”). Note that the linear318Computation Tree Logictemporal operators and U are required to be immediately preceded by ∃ or ∀ to obtaina legal state formula. Formula ∃ϕ holds in a state if there exists some path satisfying ϕthat starts in that state.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
