5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 58
Текст из файла (страница 58)
. . |= ϕ1 U ϕ2 . This remains the case ϕ2 ∈ B0 . Thenϕ1 ∈ B0 and ϕ1 U ϕ2 ∈ B0 . Assume ϕ2 ∈ Bj for all j 0. From the definition ofthe transition relation δ, we obtain using an inductive argument (successively applied to/ Bj and ϕ1 U ϕ2 ∈ Bj for j 0):ϕ1 ∈ Bj , ϕ2 ∈ϕ1 ∈ Bjand ϕ1 U ϕ2 ∈ Bjfor all j 0.282Linear Temporal LogicaB1B2a{ a, a }{ a, ¬ a }¬a¬aaaB3{ ¬a, a }B4{ ¬a, ¬ a }¬a¬aFigure 5.21: A generalised Büchi automaton for the LTL formula a.As B0 B1 B2 .
. . satisfies constraint (ii), it follows thatBj ∈ Fϕ1 U ϕ2 for infinitely many j 0.On the other hand, we haveϕ2 ∈ Bj and ϕ1 U ϕ2 ∈ Bjiff Bj ∈Fϕ1 U ϕ2for all j. Contradiction! Thus, ϕ2 ∈ Bj for some j 0. Without loss of generality, assumeϕ2 ∈ B0 , . .
. , Bj−1 , i.e., let j be the smallest index such that ϕ2 ∈ Bj . The inductionhypothesis for 0 i < j yieldsϕ1 ∈ Biandϕ1 U ϕ2 ∈ Bifor all 0 i < j.From the induction hypothesis applied to ϕ1 and ϕ2 it follows thatAj Aj+1 . . . |= ϕ2and Ai Ai+1 . . . |= ϕ1 for 0 i < j.We conclude that A0 A1 A2 . . . |= ϕ1 U ϕ2 .Example 5.38.Construction of a GNBA (Next Step)Consider ϕ = a.
The GNBA Gϕ (see Figure 5.21) is obtained as indicated in the proof ofTheorem 5.37, . The states of the automaton are the elementary sets of formulae containedinclosure(ϕ) = { a, a, ¬a, ¬ a }.Automata-Based LTL Model Checking283The state space Q consists of the following elementary setsB1 = { a, a },B3 = { ¬a, a },B2 = { a, ¬ a },B4 = { ¬a, ¬ a }.The initial states of Gϕ are the elementary sets B ∈ Q with ϕ = a ∈ B. Thus Q0 ={ B1 , B3 }. Let us justify some of the transitions. For state B1 , B1 ∩ { a } = { a }, soδ(B1 , ∅) = ∅. In addition, δ(B1 , { a }) = { B1 , B2 } since a ∈ B1 and B1 and B2 arethe only states that contain a.
As B2 ∩ { a } = { a }, we get δ(B2 , ∅) = ∅. Moreover,δ(B2 , { a }) = { B3 , B4 }. This follows from the fact that for ¬ ψ ∈ closure(ϕ), and anydirect successor B of B we have= ψ ∈ B if and only if ψ ∈ B .(This follows by the definition of δ, local consistency and maximality.) Since ¬ a ∈ B2 ,and B3 and B4 are the only states that do not contain a, we have δ(B2 , { a }) = { B3 , B4 }.Hence, δ(B4 , { a }) = ∅ since B4 ∩{ a } = ∅ = { a }. Using a similar reasoning as above, weobtain δ(B4 , ∅) = { B3 , B4 }. The outgoing transitions of B3 are determined analogously.The set F is empty as ϕ = a does not contain an until operator.
Since F = ∅, everyinfinite run in the GNBA Gϕ is accepting. As each infinite run is either of the formB1 B1 . . ., B1 B2 . . ., B3 B1 . . ., or B3 B2 . . ., and ϕ = a ∈ B1 , B2 , it follows that indeedall runs satisfy a.Example 5.39.Construction of a GNBA (Until)Consider ϕ = a U b and let AP = { a, b }. Thenclosure(ϕ) = { a, b, ¬a, ¬b, a U b, ¬(a U b) }.The construction in the proof of Theorem 5.37 yields the GNBA Gϕ illustrated in Figure 5.22. In order not to blur the figure, transition labels have been omitted.
(The labelof transition B → B equals the propositional logic formula characterising the set B ∩ AP.)The states correspond to the elementary sets of closure(ϕ)B1B2B3B4B5={ a,b,ϕ },= { ¬a,b,ϕ },={ a, ¬b,ϕ },= { ¬a, ¬b, ¬ϕ },={ a, ¬b, ¬ϕ }.The initial states are the sets Bi ∈ Q with ϕ ∈ Bi ; thus, Q0 = { B1 , B2 , B3 }. The setF = { Fϕ } of the accepting sets is a singleton, since ϕ contains a single until operator.284Linear Temporal LogicThe set Fϕ is given by/ B ∨ b ∈ B } = { B1 , B2 , B4 , B5 }.Fϕ = { B ∈ Q | ϕ ∈Since the accepting set is a singleton set, the GNBA Gϕ can be understood as an NBAwith the accepting set Fϕ .Let us justify some of the transitions.
We have B1 ∩ AP = { a, b } and a U b ∈ B1 . As:b ∈ B1 ∨ (a ∈ B1 ∧ a U b ∈ B )holds for any elementary set B ⊆ closure(a U b), we have that δ(B1 , { a, b }) contains allstates. These are the only outgoing transitions of state B1 . A similar reasoning appliesto δ(B2 , { b }). Consider state B3 . Then B3 ∩ AP = { a }. The states B that are possibledirect successors of B3 under { a } are those satisfyinga ∈ B3 ∧ a U b ∈ B .Thus, δ(B3 , { a }) = { B1 , B2 , B3 }. Finally, consider state B5 . This state only has successors for input symbol B5 ∩ AP = { a }.
For any ϕ1 U ϕ2 ∈ closure(ϕ) it can be shown thatfor any successor B of B:ϕ1 U ϕ2 ∈ Biffϕ2 ∈ B ∧ (ϕ1 ∈ B ∨ ϕ1 U ϕ2 ∈ B ).(The proof of this fact is left as an exercise.) Applying this to the state B5 yields that allstates not containing ϕ are possible successors of B5 . For example, the run B3 B3 B1 Bω4is accepting. This run corresponds to the word { a }{ a }{ a, b }∅ω which indeed satisfiesa U b. The word { a }ω does not satisfy a U b.
It has exactly one run in Gϕ , namely Bω3 . As/ Lω (Gϕ ).B3 is not a final state, this run is not accepting, i.e., { a }ω ∈Remark 5.40.Simplified Representation of the Automata StatesAny state of the GNBA for an LTL formula ϕ contains either ψ or its negation ¬ψ forevery subformula ψ of ϕ. This is somewhat redundant. It suffices to represent stateB ∈ closure(ϕ) by the propositional symbols a ∈ B ∩ AP, and the formulae ψ orϕ1 U ϕ2 ∈ B.Having constructed a GNBA Gϕ for a given LTL formula ϕ, an NBA for ϕ can be obtainedby the transformation “GNBA NBA” described in Theorem 4.56 on page 195. Recallthat this transformation for GNBA with two or more acceptance sets generates a copy ofGϕ for each acceptance set of Gϕ .
In our case, the number of copies that we need is givenby the number of until subformulae of ϕ. We obtain the following result:Automata-Based LTL Model Checking285B1{ a, b, a U b }B4{ ¬a, ¬b, ¬(a U b) }B3{ a, ¬b, a U b }B5{ a, ¬b, ¬(a U b) }{ ¬a, b, a U b }B2Figure 5.22: A generalised Büchi automaton for a U b.Theorem 5.41.Constructing an NBA for an LTL FormulaFor any LTL formula ϕ (over AP) there exists an NBA Aϕ with Words(ϕ) = Lω (Aϕ )which can be constructed in time and space 2O(|ϕ|) .Proof: From Theorem 5.37 (page 278), it follows that a GNBA Gϕ can be constructedwhich has at most 2|ϕ| states.
As the number of accepting states in Gϕ equals the numberof until-subformulas in ϕ, GNBA Gϕ has at most |ϕ| accepting states. Transforming theGNBA into an equivalent NBA (as described in the proof of Theorem 4.56, page 195),yields an NBA with at most |ϕ| copies of the state space of Gϕ . Thus, the number of statesin the NBA is at most 2|ϕ| ·|ϕ| = 2|ϕ|+log |ϕ| states. This yields the claim.There are various algorithms in the literature for associating an automaton for infinitewords to an LTL formula. The presented algorithm is one of the conceptually simplest algorithms, but often yields unnecessarily large GNBAs.
For example, for the LTL formulae a and a U b, an NBA with two states suffices. (It is left to the reader to provide theseNBAs.) Several optimizations are possible to improve the size of the resulting GNBA,but the exponential blowup cannot be avoided. This is formally stated in the followingtheorem:286Linear Temporal LogicTheorem 5.42.Lower Bound for NBA from LTL FormulaeThere exists a family of LTL formulae ϕn with |ϕn | = O(poly (n)) such that every NBAfor ϕn has at least 2n states.Proof: Let AP be an arbitrary nonempty set of atomic propositions, that is, |2AP | 2.Consider the family of languages:Ln = { A1 .
. . An A1 . . . An σ | Ai ⊆ AP ∧ σ ∈ (2AP )ω },for n 0.It is not difficult to check that Ln = Words(ϕn ) where( i a ←→ n+i a).ϕn =a∈AP 0i<nHere, j stands for the j-fold application of the next-step operator , i.e., 1 ϕ = ϕand n+1 ϕ = n ϕ. It follows that ϕn is an LTL formula of polynomial length. Moreprecisely, |ϕn | ∈ O(|AP| · n).However, any NBA A with Lω (A) = Ln has at least 2n states. Essentially, this is justifiedby the following consideration.
Since the wordsA1 . . . An A1 . . . An ∅ ∅ ∅ . . .are accepted by A, A contains for every word A1 . . . An of length n, a state q(A1 . . . An ),which can be reached from an initial state by consuming the prefix A1 . . . An . Startingfrom q(A1 . . . An ) it is possible to visit an accept state infinitely often by accepting thesuffix A1 .
. . An ∅ ∅ ∅ . . .. If A1 . . . An = A1 . . . An then/ Ln = Lω (A).A1 . . . An A1 . . . An ∅ ∅ ∅ . . . ∈Therefore, the states q(A1 . . . An ) are all pairwise different. As there are |2AP | possiblecombinations for A1 . . . An , A has at least (|2AP |)n 2n states.Remark 5.43.Büchi Automata are More Expressive Than LTLThe results so far show that for every LTL formula ϕ an NBA can be constructed thataccepts exactly the infinite sequences satisfying ϕ. We state without proof that the reverse,however, is not true. It can be shown that for, e.g., the LT propertyP = A0 A1 A2 . .
. ∈ (2{ a } )ω | a ∈ A2i for i 0 ,which requires a to hold in every even position, there is no LTL formula ϕ with Words(ϕ) =P . On the other hand, there exists an NBA A with Lω (A) = P . (It is left to the readerto provide such an NBA.)Automata-Based LTL Model Checking5.2.1287Complexity of the LTL Model-Checking ProblemLet us summarize the results of the previous sections in order to provide an overview ofLTL model checking. Subsequently, we discuss the complexity of the LTL model-checkingproblem.As explained before, the essential idea behind the automata-based model-checking algorithm for LTL is based upon the following relations:TS |= ϕ iff Traces(TS) ⊆ Words(ϕ)iff Traces(TS) ⊆ (2AP )ω \ Words(¬ϕ)iff Traces(TS) ∩ Words(¬ϕ) = ∅Lω (A¬ϕ )iff TS ⊗ A¬ϕ |= ♦ ¬F.Here, NBA A¬ϕ accepts Words(¬ϕ) and F is its set of accept states.
The algorithm totransform an LTL formula ϕ into an NBA may give rise to an NBA whose state space sizeis exponential in the length of ϕ. The NBA A¬ϕ can thus be constructed in exponentialtime:O(2|ϕ| · |ϕ|) = O(2|ϕ|+ log |ϕ| ).This complexity bound, together with the fact that the state space of A is exponential in|ϕ|, yields an upper bound for the time- and space-complexity of LTL model checking (seeAlgorithm 11, page 272):O( |TS| · 2|ϕ| ).Remark 5.44.LTL Model Checking with FairnessAs a consequence of Theorem 5.30 (see page 264), the model-checking problem for LTLwith fairness assumptions can be reduced to the model-checking problem for plain LTL.So, in order to check the formula ϕ under fairness assumption fair , it suffices to verifythe formula fair → ϕ with an LTL model-checking algorithm.
This approach, however,has as its main drawback that the length |fair | can have an exponential influence on therun-time of the algorithm. This is due to the construction of an NBA for the negatedformula, i.e., ¬(fair → ϕ), whose size is exponential in |¬(fair → ϕ)| = |fair | + |ϕ|. Toavoid this additional exponential blowup, a modified persistence check (see Algorithm 8on page 211) can be exploited to analyze the product transition system TS ⊗ A¬ϕ (insteadof TS ⊗ A¬(fair →ϕ) ). This can be done using standard graph algorithms.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
