5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 56
Текст из файла (страница 56)
The latter happens, e.g., in the pathologicalcase where only the mutator acts infinitely often. To rule out this unrealistic behavior,weak process fairness can be imposed.5.2Automata-Based LTL Model CheckingIn this section we address the model-checking problem for LTL. The starting point is afinite transition system TS and an LTL formula ϕ that formalizes a requirement on TS.The problem is to check whether TS |= ϕ. If ϕ is refuted, an error trace needs to beprovided for debugging purposes.
The considerations in Section 2.1 show that transitionAutomata-Based LTL Model Checking271systems are typically huge. Therefore, a manual proof of TS |= ϕ is extremely difficult.Instead, verification tools are desirable, which enable a fully automated analysis of thetransition system.In general, not just a single requirement but several requirements are relevant. Theserequirements can be represented by separate formulae, such as ϕ1 , . . . , ϕk , and be combined into ϕ1 ∧ . . . ∧ ϕk to obtain a specification of all requirements. Alternatively, therequirements ϕi can be treated separately.
This is often more efficient than consideringthem together. Moreover, the decomposition of the entire requirement specification intoseveral requirements is advised if errors are to be expected or if the validity of ϕi is knownby a prior analysis.An LTL model-checking algorithm is a decision procedure which for a transition system TSand LTL formula ϕ returns the answers “yes” if TS |= ϕ, and “no” (plus a counterexample)if TS |= ϕ. The counterexample consists of an appropriate finite prefix of an infinite pathin TS where ϕ does not hold. Theorem 5.30 shows that special measures to handle fairnessassumptions are unnecessary as fairness assumptions can be encoded in the LTL formulato be checked. (For reasons of efficiency, however, it is advised to use special algorithmsto treat fairness assumptions.)Throughout this section, TS is assumed to be finite and to have no terminal states. Themodel-checking algorithm presented in the following is based on the automata-based approach as originally suggested by Vardi and Wolper (1986).
This approach is based on thefact that each LTL formula ϕ can be represented by a nondeterministic Büchi automaton(NBA). The basic idea is to try to disprove TS |= ϕ by “looking” for a path π in TS withπ |= ¬ϕ. If such a path is found, a prefix of π is returned as error trace. If no such pathis encountered, it is concluded that TS |= ϕ.The essential steps of the model-checking algorithm as summarized in Algorithm 11 andFigure 5.16, rely on the following observations:TS |= ϕiffTraces(TS) ⊆ Words(ϕ)iffTraces(TS) ∩ ((2AP )ω \ Words(ϕ)) = ∅iffTraces(TS) ∩ Words(¬ϕ) = ∅.Hence, for NBA A with Lω (A) = Words(¬ϕ) we haveTS |= ϕif and only if Traces(TS) ∩ Lω (A) = ∅.Thus, to check whether ϕ holds for TS one first constructs an NBA for the negation ofthe input formula ϕ (representing the ”bad behaviors”) and then applies the techniquesexplained in Chapter 4 for the intersection problem.272Linear Temporal LogicAlgorithm 11 Automaton-based LTL model checkingInput: finite transition system TS and LTL formula ϕ (both over AP)Output: “yes” if TS |= ϕ; otherwise, “no” plus a counterexampleConstruct an NBA A¬ϕ such that Lω (A¬ϕ ) = Words(¬ϕ)Construct the product transition system TS ⊗ Aif there exists a path π in TS ⊗ A satisfying the accepting condition of A thenreturn “no” and an expressive prefix of πelsereturn “yes”fiIt remains to explain how a given LTL formula can be represented by an NBA and howsuch an NBA can be constructed algorithmically.
First observe that for the LTL formulaϕ, the LTL semantics provided in Definition 5.6 on page 235 yields a language Words(ϕ) ⊆(2AP )ω . Thus, the alphabet of NBA for LTL formulae is Σ = 2AP . The next step is toshow that Words(ϕ) is ω-regular, and hence, representable by a nondeterministic Büchiautomaton.Example 5.32.NBA for LTL FormulaeBefore treating the details of transforming an LTL formula into an NBA, we providesome examples.
As in Chapter 4, propositional logic formulae are used (instead of the setnotations) for a symbolic representation of the edges of an NBA. These formulae are builtby the symbols a ∈ AP, the constant true, and the Boolean connectors, and thus theycan be interpreted over sets of atomic propositions, i.e., the elements A ∈ Σ = 2AP .
Fora∨b−→ q is a short notation for the three transitions:instance, if AP = { a, b } then q −−{a}{b}{a,b}q −−−→ q , q −−−→ q , and q −−−−→ q .The language of all words σ = A0 A1 . . . ∈ 2AP satisfying the LTL formula ♦green(“infinitely often green”) is accepted by the NBA A shown in Figure 5.17. Here, AP isa set of atomic propositions containing green. Note that A is in the accept state q1 ifand only if the last consumed symbol (the last set Ai of the input word A0 A1 A2 . . . ∈(2AP )ω ) contains the propositional symbol green. Therefore, the accepted language Lω (A)is exactly the set of all infinite words A0 A1 A2 .
. . with infinitely many indices i wheregreen ∈ Ai . Thus,Lω (A) = Words(♦green).The accepting run that generates the word σ = { green }∅{ green }∅ . . . is (q0 q1 )ω .Automata-Based LTL Model Checking273Negation of propertySystemLTL-formula ¬ϕModel of systemmodel checkerGeneralised Büchi automatonBüchi automaton A¬ϕTransition system TSProduct transition systemTS ⊗ A¬ϕTS ⊗ A |= Ppers(A)‘No’ (counter-example)‘Yes’Figure 5.16: Overview of LTL model checking.greenq0¬ greenq1¬greengreenFigure 5.17: NBA for ♦green.As a second example consider the liveness property: “whenever event a occurs, event bwill eventually occur”. For example, the property given by the LTL formula (request →♦response) is of this form.
An associated NBA over the alphabet 2{a,b} where a = requestand b = response is shown in Figure 5.18.The automata in Figures 5.17 and 5.18 are deterministic, i.e., they have exactly one runfor each input word. To represent temporal properties like “eventually forever (from somemoment on)”, the concept of nondeterminism is, however, necessary.The NBA A shown in Figure 5.19 accepts the language Words(♦a).
Here, AP ⊇ { a } andΣ = 2AP ; see also Example 4.51 (page 191). Intuitively, the NBA A nondeterministicallydecides (by means of an omniscient oracle) when a continuously holds. Note that state q2may be omitted, as there is no accepting run beginning in q2 . (The reader should bear inmind that DBA and NBA are not equally expressive; see Section 4.3.3 on page 188.)274Linear Temporal Logica ∧ ¬bq0q1¬a ∨ bb¬bFigure 5.18: NBA for (a → ♦b).aq0trueq1¬aaq2trueFigure 5.19: NBA for ♦a.A key ingredient to the model-checking algorithm for LTL is the construction of an NBAA satisfyingLω (A) = Words(ϕ)for the LTL formula ϕ.
In order to do so, first a generalized NBA is constructed for ϕ,which subsequently is transformed into an equivalent NBA. For the latter step we employthe recipe as provided in Theorem 4.56 on page 195. For the sake of convenience we recallthe definition of generalized NBA; see also Definition 4.52 on page 193.Definition 5.33.Generalized NBA (GNBA)A generalized NBA is a tuple G = (Q, Σ, δ, Q0 , F) where Q, Σ, δ, Q0 are defined as forNBA (i.e., Q is a finite state space, Σ an alphabet, Q0 ⊆ Q the set of initial states, andδ : Q × Σ → 2Q the transition relation) and F is a (possibly empty) subset of 2Q . Theelements of F are called acceptance sets. The accepted language Lω (G) consists of allinfinite words in (2AP )ω that have at least one infinite run q0 q1 q2 .
. . in G such that foreach acceptance set F ∈ F there are infinitely many indices i with qi ∈ F .A GNBA for which F is a singleton set can be regarded as an NBA. If the set F ofacceptance sets in G is empty, the language Lω (G) consists of all infinite words that havean infinite run in G. Hence, if F = ∅, then G can be viewed as an NBA for which allstates are accepting.Let us consider how to construct a GNBA over the alphabet 2AP for a given LTL formulaϕ (over AP), i.e., a GNBA Gϕ with Lω (Gϕ ) = Words(ϕ). Assume ϕ only contains theoperators ∧, ¬, and U , i.e., the derived operators ∨, →, ♦, , W , and so on areassumed to be expressed in terms of the basic operators. Since the special case ϕ = trueis trivial, it may be assumed that ϕ = true.Automata-Based LTL Model Checking275The basic idea for the construction of Gϕ is as follows.
Let σ = A0 A1 A2 . . . ∈ Words(ϕ).The sets Ai ⊆ AP are expanded by subformulae ψ of ϕ such that an infinite word σ̄ =B0 B1 B2 . . . with the following property arises:ψ ∈ Biif and only ifA A A . . . |= ψ. i i+1 i+2 σiFor technical reasons, the subformulae ψ of ϕ are considered as well as their negation ¬ψ.Consider, e.g.,ϕ = a U (¬a ∧ b) and σ = { a } { a, b } { b } .
. . .In this case, Bi is a subset of the set of formulae{ a, b, ¬a, ¬a ∧ b, ϕ } ∪ { ¬b, ¬(¬a ∧ b), ¬ϕ } . subformulae of ϕtheir negationThe set A0 = { a } is extended with the formulae ¬b, ¬(¬a ∧ b), and ϕ, since all theseformulae hold in σ 0 = σ, and all other subformulae in the above set are refuted by σ. Wethus obtainB0 = { a, ¬b, ¬(¬a ∧ b), ϕ }.The set A1 = { a, b } is extended with ¬(¬a ∧ b) and ϕ, as these are the only subformulaein the above set that hold in σ 1 = { a, b } { b } . . ..
The A2 = { b } is extended with ¬a,¬a ∧ b and ϕ as they hold in σ 2 = { b } . . .. This yields a word of the form:σ̄ = { a, ¬b, ¬(¬a ∧ b), ϕ } { a, b, ¬(¬a ∧ b), ϕ } { ¬a, b, ¬a ∧ b, ϕ } . . .As σ is infinite, this procedure is of course not effective. The example is just meant toexplain the intuition behind the construction of the states in the GNBA.The GNBA Gϕ is constructed such that the sets Bi constitute its states. Moreover, theconstruction ensures that σ̄ = B0 B1 B2 . . . is a run for σ = A0 A1 A2 . . . in Gϕ .
Theaccepting conditions for Gϕ are chosen such that the run σ̄ is accepting if and only if σ |= ϕ.Thus, we have to encode the meaning of the logical operators into the states, transitions,and acceptance sets of Gϕ . The meaning of propositional logic operators ∧, ¬, and theconstant true will be encoded in the states by requiring consistent formula sets Bi .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
