5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 57
Текст из файла (страница 57)
Thesemantics of the next-step operator relies on a nonlocal condition and will be encoded in thetransition relation. The meaning of the until operator is split according to the expansionlaw into local conditions (encoded in the states) and a next-step condition (encoded in thetransitions). Since the expansion law does not provide a full characterization of until, afurther condition is imposed which expresses the fact that the meaning of until yields theleast solution of the expansion law (see Lemma 5.18 on page 251). This will be encodedby the acceptance sets of Gϕ .276Linear Temporal LogicAs explained above, the formula sets are subsets of subformulae of ϕ and their negation.Definition 5.34.Closure of ϕThe closure of LTL formula ϕ is the set closure(ϕ) consisting of all subformulae ψ of ϕand their negation ¬ψ (where ψ and ¬¬ψ are identified).For instance, for ϕ = a U (¬a ∧ b), the set closure(ϕ) consists of the formulaea, b, ¬a, ¬b, ¬a ∧ b, ¬(¬a ∧ b), ϕ, ¬ϕ.It is not difficult to assess that |closure(ϕ)| ∈ O(|ϕ|).
A set of formulae B ⊆ closure(ϕ)is called elementary if B is the set of all formulae ψ ∈ closure(ϕ) with π |= ψ for a pathπ. For this, B should not contain propositional logic contradictions and it must be locallyconsistent with respect to the until operator. Since for any path π and formula ψ, eitherπ |= ψ or π |= ¬ψ, it is additionally required that elementary sets of formulae are maximal.The precise definition of these three conditions is provided in Figure 5.20 on page 277.Definition 5.35.Elementary Sets of FormulaeB ⊆ closure(ϕ) is elementary if it is consistent with respect to propositional logic, maximal, and locally consistent with respect to the until operator.The requirements for local consistency result from the expansion lawϕ1 U ϕ2 ≡ ϕ2 ∨ (ϕ1 ∧ (ϕ1 U ϕ2 )).Due to the required maximality and propositional logic consistency, we haveψ ∈ Bif and only if ¬ψ ∈ Bfor all elementary sets B and subformulae ψ of ϕ.
Further, due to maximality and localconsistency, we have/ B.ϕ1 , ϕ2 ∈ B implies ϕ1 U ϕ2 ∈Hence, if ϕ1 , ϕ2 ∈ B then { ¬ϕ1 , ¬ϕ2 , ¬(ϕ1 U ϕ2 ) } ⊆ B; here, it is assumed that ϕ1 U ϕ2is a subformula of ϕ.Example 5.36.Elementary Sets of FormulaeLet ϕ = a U (¬a ∧ b). The set B = { a, b, ϕ } ⊆ closure(ϕ) is consistent with respect topropositional logic and locally consistent with respect to the until operator. It is, however,not maximal, since for ¬a ∧ b ∈ closure(ϕ):¬a ∧ b ∈/Band¬(¬a ∧ b) ∈/ B.Automata-Based LTL Model Checking2771. B is consistent with respect to propositional logic, i.e., for allϕ1 ∧ ϕ2 , ψ ∈ closure(ϕ):• ϕ1 ∧ ϕ2 ∈ B ⇔ ϕ1 ∈ B and ϕ2 ∈ B• ψ ∈ B ⇒ ¬ψ ∈ B• true ∈ closure(ϕ) ⇒ true ∈ B.2.
B is locally consistent with respect to the until operator, i.e.,for all ϕ1 U ϕ2 ∈ closure(ϕ):• ϕ2 ∈ B ⇒ ϕ1 U ϕ2 ∈ B• ϕ1 U ϕ2 ∈ B and ϕ2 ∈ B ⇒ ϕ1 ∈ B.3. B is maximal, i.e., for all ψ ∈ closure(ϕ):• ψ∈/ B ⇒ ¬ψ ∈ B.Figure 5.20: Properties of elementary sets of formulae.The set of formulae { a, b, ¬a ∧ b, ϕ } contains the propositional logic “contradiction” a and¬a ∧ b and therefore is not elementary. The set{¬a, ¬b, ¬(¬a ∧ b), ϕ}is consistent with respect to propositional logic but contains a local inconsistency withrespect to the until operator U , since a U (¬a ∧ b) ∈ B and ¬a ∧ b ∈ B, but a ∈ B.
Thismeans thatπ |= ¬a, π |= ¬(¬a ∧ b), and π |= ϕare impossible for any path π.The following sets are elementary:B1B2B3B4B5B6======{a,b, ¬(¬a ∧ b),ϕ },{a,b, ¬(¬a ∧ b), ¬ϕ },{a, ¬b, ¬(¬a ∧ b),ϕ },{a, ¬b, ¬(¬a ∧ b), ¬ϕ },{ ¬a, ¬b, ¬(¬a ∧ b), ¬ϕ },{ ¬a,b,¬a ∧ b,ϕ }.The proof of the following theorem shows how to construct for an arbitrary LTL formula ϕa GNBA Gϕ with Lω (Gϕ ) = Words(ϕ). This construction is one of the initial steps of the278Linear Temporal LogicLTL model checking algorithm; see Figure 5.16 (page 273). Subsequently, the resultingGNBA Gϕ is transformed into an NBA Aϕ by means of the technique indicated in theproof of Theorem 4.56 (page 195).Theorem 5.37.GNBA for LTL FormulaFor any LTL formula ϕ (over AP) there exists a GNBA Gϕ over the alphabet 2AP suchthat(a) Words(ϕ) = Lω (Gϕ ).(b) Gϕ can be constructed in time and space 2O(|ϕ|) .(c) The number of accepting sets of Gϕ is bounded above by O(|ϕ|).Proof: Let ϕ be an LTL formula over AP.
Let Gϕ = (Q, 2AP , δ, Q0 , F) where• Q is the set of all elementary sets of formulae B ⊆ closure(ϕ),• Q0 = { B ∈ Q | ϕ ∈ B },• F = { Fϕ1 U ϕ2 | ϕ1 U ϕ2 ∈ closure(ϕ)} whereFϕ1 U ϕ2 = { B ∈ Q | ϕ1 U ϕ2 ∈ B or ϕ2 ∈ B }.The transition relation δ : Q × 2AP → 2Q is given by:• If A = B ∩ AP, then δ(B, A) = ∅.• If A = B ∩ AP, then δ(B, A) is the set of all elementary sets of formulae B satisfying(i) for every ψ ∈ closure(ϕ): ψ ∈ B ⇔ ψ ∈ B , and(ii) for every ϕ1 U ϕ2 ∈ closure(ϕ):ϕ1 U ϕ2 ∈ B ⇔ (ϕ2 ∈ B ∨ (ϕ1 ∈ B ∧ ϕ1 U ϕ2 ∈ B )).The constraints (i) and (ii) reflect the semantics of the next-step and the until operator,respectively. Rule (ii) is justified by the expansion law:ϕ1 U ϕ2 ≡ ϕ2 ∨ (ϕ1 ∧ (ϕ1 U ϕ2 )).Automata-Based LTL Model Checking279To model the semantics of U , an acceptance set Fψ is introduced for every subformulaψ = ϕ1 U ϕ2 of ϕ.
The underlying idea is to ensure that in every run B0 B1 B2 . . . for whichψ ∈ B0 , we have ϕ2 ∈ Bj (for some j 0) and ϕ1 ∈ Bi for all i < j. The requirementthat a word σ satisfies ϕ1 U ϕ2 only if ϕ2 will actually eventually become true is ensuredby the accepting set Fϕ1 U ϕ2 .Let us first consider the claim (b). States in the GNBA Gϕ are elementary sets of formulaein closure(ϕ).
Let subf(ϕ) denote the set of all subformulae of ϕ. The number of states inGϕ is bounded by 2|subf(ϕ)| , the number of possible formula sets. (The elementary formulasets B can be represented by bit vectors containing a single bit per subformula ψ of ϕwhich indicates whether ψ or ¬ψ belongs to B.) As |subf(ϕ)| 2·|ϕ|, the number of statesin the GNBA Gϕ is bounded by 2O(|ϕ|) . Claim (c) follows directly from the fact that thenumber of accept sets is equal to the number of until-subformulae in ϕ.It remains to show that (a) Lω (Gϕ ) = Words(ϕ). We prove set inclusion in both directions.⊇: Let σ = A0 A1 A2 . .
. ∈ Words(ϕ). Then, σ ∈ (2AP )ω and σ |= ϕ. The elementary setBi of formulae is defined as follows:Bi = { ψ ∈ closure(ϕ) | Ai Ai+1 . . . |= ψ }(5.1)Obviously, Bi is an elementary set of formulae, i.e., Bi ∈ Q. We now prove that B0 B1 B2 . . .is an accepting run for σ. Observe that Bi+1 ∈ δ(Bi , Ai ) for all i 0, since for all i:• Ai = Bi ∩ AP• for ψ ∈ closure(ϕ): ψ ∈ Biiff(* equation (5.1) for Bi *)Ai Ai+1 . . .
|= ψiffAi+1 Ai+2 . . . |= ψ(* semantics of *)(* equation (5.1) for Bi+1 *)iffψ ∈ Bi+1280Linear Temporal Logic• for ϕ1 U ϕ2 ∈ closure(ϕ):ϕ1 U ϕ2 ∈ Biiff(* equation (5.1) for Bi *)Ai Ai+1 . . . |= ϕ1 U ϕ2iff(* semantics of until *)Ai Ai+1 . . . |= ϕ2 or)Ai Ai+1 . . . |= ϕ1 and (Ai+1 Ai+2 . .
. |= ϕ1 U ϕ2iff(* equation (5.1) for Bi and Bi+1 *)ϕ2 ∈ Bi or (ϕ1 ∈ Bi and ϕ1 U ϕ2 ∈ Bi+1 ).This shows that B0 B1 B2 . . . is a run of Gϕ . It remains to prove that this run is accepting,i.e., for each subformula ϕ1,j U ϕ2,j in closure(ϕ), Bi ∈ Fj for infinitely many i. Bycontraposition. Assume there are finitely many i such that Bi ∈ Fj .
We have:/ Fj = Fϕ1,j U ϕ2,j ⇒ ϕ1,j U ϕ2,j ∈ Bi and ϕ2,j ∈/ Bi .Bi ∈As Bi = { ψ ∈ closure(ϕ) | Ai Ai+1 . . . |= ψ }, it follows that if Bi ∈ Fj , then:Ai Ai+1 . . . |= ϕ1,j U ϕ2,jandAi Ai+1 . . . |= ϕ2,j .Thus, Ak Ak+1 . . . |= ϕ2,j for some k > i. By definition of the formula sets Bi , it thenfollows that ϕ2,j ∈ Bk , and by definition of Fj , Bk ∈ Fj . Thus, Bi ∈ Fj for finitely manyi, then Bk ∈ Fj for infinitely many k. Contradiction.Thus, B0 B1 B2 . .
. is an accepting run of Gϕ , and hence, A0 A1 A2 . . . ∈ Lω (Gϕ ).⊆: Let σ = A0 A1 A2 . . . ∈ Lω (Gϕ ), i.e., there is an accepting run B0 B1 B2 . . ., say, for σin Gϕ . Sinceδ(B, A) = ∅for all pairs (B, A) with A = B ∩ AP,it follows that Ai = Bi ∩ AP for i 0. Thusσ = (B0 ∩ AP) (B1 ∩ AP) (B2 ∩ AP) . . .Our proof obligation now becomes (B0 ∩ AP) (B1 ∩ AP) (B2 ∩ AP) .
. . |= ϕ. We provethe following more general proposition:Automata-Based LTL Model Checking281For B0 B1 B2 . . . a sequence with Bi ∈ Q satisfying(i) for all i 0 : Bi+1 ∈ δ(Bi , Ai ), and∞(ii) for all F ∈ F : ∃ j 0. Bj ∈ F ,we have for all ψ ∈ closure(ϕ):ψ ∈ B0⇔A0 A1 A2 . . . |= ψ.The proof of this claim is by structural induction on the structure of ψ.Base case: The statement for ψ = true or ψ = a with a ∈ AP follows directly fromequation (5.1) and the definition of closure.Induction step: Based on the induction hypothesis that the claim holds for ψ , ϕ1 , ϕ2 ∈closure(ϕ), it is proven that for the formulaeψ = ψ , ψ = ¬ψ , ψ = ϕ1 ∧ ϕ2 and ψ = ϕ1 U ϕ2the claim also holds.
We provide the detailed proof for ψ = ϕ1 U ϕ2 . Let A0 A1 A2 . . . ∈(2AP )ω and B0 B1 B2 . . . ∈ Qω satisfying the constraints (i) and (ii). It is now shown that:ψ ∈ B0iffA0 A1 A2 . . . |= ψ.This goes as follows.⇐: Assume A0 A1 A2 . . . |= ψ where ψ = ϕ1 U ϕ2 . Then, there exists j 0 such thatAj Aj+1 . .
. |= ϕ2and Ai Ai+1 . . . |= ϕ1 for 0 i < j.From the induction hypothesis (applied to ϕ1 and ϕ2 ) it follows thatϕ2 ∈ Bjandϕ1 ∈ Bifor 0 i < j.By induction on j we obtain: ϕ1 U ϕ2 ∈ Bj , Bj−1 . . . , B0 .⇒: Assume ϕ1 U ϕ2 ∈ B0 . Since B0 is elementary, ϕ1 ∈ B0 or ϕ2 ∈ B0 . Distinguishbetween ϕ2 ∈ B0 and ϕ2 ∈ B0 . If ϕ2 ∈ B0 , it follows from the induction hypothesisA0 A1 . . . |= ϕ2 , and thus A0 A1 .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
