5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 37
Текст из файла (страница 37)
−−−−→ qn+1q0 −−−−is a run—not necessarily accepting—of NFA A that generates the wordtrace(π) = L(s0 ) L(s1 ) . . . L(sn ).Finally, labels of states are state names of A. These considerations lead to the followingdefinition:Model-Checking Regular Safety PropertiesDefinition 4.16.165Product of Transition System and NFALet TS = (S, Act, →, I, AP, L) be a transition system without terminal states and A =(Q, Σ, δ, Q0 , F ) an NFA with the alphabet Σ = 2AP and Q0 ∩ F = ∅. The producttransition system TS ⊗ A is defined as follows:TS ⊗ A = (S , Act, → , I , AP , L )where• S = S × Q,• → is the smallest relation defined by the ruleL(t)α→ t ∧ q −−−→ ps −−,α s, q −−→ t, pL(s )0→ q },• I = { s0 , q | s0 ∈ I ∧ ∃q0 ∈ Q0 .
q0 −−−−• AP = Q, and• L : S × Q → 2Q is given by L (s, q) = { q }.Remark 4.17.Terminal StatesFor the definition of LT properties (and thus of invariants) we have assumed transitionsystems to have no terminal states. It is, however, not guaranteed that TS ⊗ A possessesthis property, even if TS does. This stems from the fact that in NFA A there may be a stateq, say, that has no direct successor states for some set A of atomic propositions, i.e., withδ(q, A) = ∅. This technical problem can be treated by either requiring δ(q, A) = ∅ for allstates q ∈ Q and A ⊆ AP or by extending the notion of invariants to arbitrary transitionsystems.
Note that imposing the requirement δ(q, A) = ∅ is not a severe restriction, asany NFA can be easily transformed into an equivalent one that satisfies this property byA→ qtrap to A whenever δ(q, A) = ∅ orintroducing a state qtrap and adding transition q −−q = qtrap . We finally remark that for the algorithm for invariant checking, it is not of anyrelevance whether terminal states exist or not.Example 4.18.A Product AutomatonThe language of the minimal bad prefixes of the safety property “each red light phase166Regular Propertiesyellow¬red ∧ ¬yellowyellow ∧ ¬redredred/yellowyellowq1q0¬yellowredqFgreengreen, q0 red/yellow, q0 yellow, q1 red, q0 Figure 4.6: German traffic light (left upper figure), an NFA (right upper figure), and theirproduct (lower figure).is preceded by a yellow light phase” is accepted by the DFA A indicated in Example4.14 (page 162).
We consider a German traffic light, which besides the usual possiblecolors red, green, and yellow, has the possibility to indicate red and yellow simultaneouslyindicating “green light soon”. The transition system GermanTrLight thus has four stateswith the usual transitions red → red+yellow, red+yellow → green, green → yellow,and yellow → red. Let AP = { red, yellow } indicating the corresponding light phases.The labeling is defined as follows: L(red) = { red }, L(yellow) = { yellow }, L(green) =∅ = L(red+yellow). The product transition system GermanTrLight ⊗ A consists of fourreachable states (see Figure 4.6). As action labels are not relevant here, they are omitted.The following theorem shows that the verification of a regular safety property can bereduced to checking an invariant in the product.Let TS and A be as before.
Let Pinv (A) be the invariant over AP = 2Q which is definedby the propositional formula¬ q.q∈FIn the sequel, we often write ¬ F as shorthand forin all nonaccept states.q∈F¬ q. Stated in words, ¬F holdsModel-Checking Regular Safety PropertiesTheorem 4.19.167Verification of Regular Safety PropertiesFor transition system TS over AP, NFA A with alphabet 2AP as before, and regular safetyproperty Psafe over AP such that L(A) equals the set of (minimal) bad prefixes of Psafe ,the following statements are equivalent:(a) TS |= Psafe(b) Tracesfin (TS) ∩ L(A) = ∅(c) TS ⊗ A |= Pinv (A)Proof: Let TS = (S, Act, →, I, AP, L) and A = (Q, 2AP , δ, Q0 , F ).The equivalence of (a) and (b) follows immediately by Lemma 3.25 (page 114).
To establishthe equivalence of (a), (b), and (c), we show(c) =⇒ (a) : TS |= PsafeTS ⊗ A |= Pinv (A)impliesand(b) =⇒ (c) : TS ⊗ A |= Pinv (A)impliesTracesfin (TS) ∩ L(A) = ∅. =Proof of “(c) =⇒ (a)”: If TS |= Psafe , then there is a finite initial path fragment πs0 s1 . . . sn in TS withtrace(π ) = L(s0 ) L(s1 ) . . . L(sn ) ∈ L(A).π ).Since trace(π ) ∈ L(A), there exists an accepting run q0 q1 . . .
qn+1 of A for trace(AccordinglyL(s )i→ qi+1 for all 0 i n, and qn+1 ∈ F.q0 ∈ Q0 and qi −−−−Thus, s0 , q1 s1 , q2 . . . sn , qn+1 is an initial path fragment in TS ⊗ A withsn , qn+1 |= ¬F.It thus follows that TS ⊗ A |= Pinv (A) .Proof of “(b) =⇒ (c)”: Let TS ⊗ A |= Pinv (A) . Then there exists an initial path fragments0 , q1 .
. . sn , qn+1 in TS ⊗ A with qn+1 ∈ F , and q1 , . . . , qn ∈ F . Besides, s0 s1 . . . sn is an initial pathfragment in TS. Further,168Regular PropertiesL(s )iqi −−−−→ qi+1 for all 0 i n.Since s0 , q1 is an initial state of TS ⊗ A, there is an initial state q0 in A such thatL(s0 )q0 −−−−→ q1 . Sequence q0 q1 . . . qn+1 is thus an accepting run for trace(s0 s1 . . . sn ). Thus,trace(s0 s1 . . . sn ) ∈ Tracesfin (TS) ∩ L(A)which yields Tracesfin (TS) ∩ L(A) = ∅.Stated in words, Theorem 4.19 yields that in order to check the transition system TSversus the regular safety property Psafe , it suffices to check whether no state s, q inTS ⊗ A is reachable where the A-component q is an accept state in A.
This invariant“visit never an accept state in A” (formally given by the invariant condition Φ = ¬F )can be checked using a depth-first search approach as described in detail in Algorithm 4(page 110). Note that in case the safety property is refuted, the invariant checking algorithm provides a counterexample. This counterexample is in fact a finite path fragments0 , q1 s1 , q2 . .
. sn , qn+1 in the transition system TS ⊗ A that leads to an accept state.The projection to the states in TS yields an initial finite path fragment s0 s1 . . . sn in TSwhere the induced trace trace(s0 s1 . . . sn ) ∈ (2AP )∗ is accepted by A (since it has an accepting run of the form q0 q1 . . . qn+1 ). Thus, trace(s0 s1 . . . sn ) is a bad prefix for Psafe ./ Psafe for all paths π inHence, s0 s1 .
. . sn yields a useful error indication since trace(π) ∈TS that start with the prefix s0 s1 . . . sn .Corollary 4.20.Let TS, A, and Psafe be as in Theorem 4.19. Then, for each initial path fragment s0 , q1 . . .sn , qn+1 of TS ⊗ A:q1 , . . . , qn ∈ F and qn+1 ∈ Fimpliestrace(s0 s1 . . . sn ) ∈ L(A).As a result, the skeleton in Algorithm 5 can be used to check a regular safety propertyagainst a transition system and to report a counterexample (i.e., finite initial path fragmentin TS inducing a bad prefix) as diagnostic feedback if the safety property does not holdfor TS.Example 4.21.Checking a Regular Safety Property for the Traffic LightConsider again the German traffic light system and the regular safety property PsafeModel-Checking Regular Safety Properties169Algorithm 5 Model-checking algorithm for regular safety propertiesInput: finite transition system TS and regular safety property PsafeOutput: true if TS |= Psafe .
Otherwise false plus a counterexample for Psafe .Let NFA A (with accept states F ) be such that L(A) = bad prefixes of PsafeConstruct the product transition system TS ⊗ A Check the invariant Pinv (A) with proposition ¬F = q∈F ¬q on TS ⊗ A.if TS ⊗ A |= Pinv (A) thenreturn trueelseDetermine an initial path fragment s0 , q1 . . . sn , qn+1 of TS ⊗ A with qn+1 ∈ Freturn (false, s0 s1 . . .
sn )fithat each red light phase should be immediately preceded by a yellow light phase. Thetransition system of the traffic light, the NFA accepting the bad prefixes of the safetyproperty, as well as their product automaton, are depicted in Figure 4.6 (page 166). Tocheck the validity of Psafe , only the second component of the states s, q is relevant. Thefact that no state of the form . .
. , qF is reachable ensures the invariant ¬qF to hold inall reachable states. Thus GermanTrLight |= Psafe .If the traffic light is modified such that the state “red” is the initial state (instead of“green”), then we obtain a transition system that violates Psafe . Actually, in this casethe invariant ¬qF is already violated in the initial state of the resulting product transitionsystem that has the following form:red, δ(q0 , {red}) = red, qF .We conclude this part by considering the worst-case time and space complexity of theautomata-based algorithm for checking regular safety properties.Theorem 4.22.Complexity of Verifying Regular Safety PropertiesThe time and space complexity of Algorithm 5 is in O(|TS|·|A|) where |TS| and |A| denotethe number of states and transitions in TS and A, respectively.Assuming an generation of the reachable states of TS from a syntactic description of theprocesses, the above bound also holds if |TS| denotes the size of the reachable fragmentof TS.170Regular PropertiesProof: Follows directly from the fact that the number of states in the product automatonTS ⊗ A is in O(|S|·|Q|) (where S and Q denote the state space of TS and A, respectively)and the fact that the time and space complexity of invariant checking is linear in thenumber of states and transitions of the transition system TS ⊗ A.
(Thus, we can evenestablish the bound O(|S|·|Q| + | → |·|δ|) for the runtime where | → | denotes the numberof transitions in TS and |δ| the number of transitions in A.)4.3Automata on Infinite WordsFinite-state automata accept finite words, i.e., sequences of symbols of finite length, andyield the basis for checking regular safety properties. In this and the following sections,these ideas are generalized toward a more general class of LT properties. These includeregular safety, various liveness properties, but also many other properties that are relevantto formalize the requirements for “realistic” systems. The rough idea is to consider variantsof NFAs, called nondeterministic Büchi automata (NBAs), which serve as acceptors forlanguages of infinite words.
It will be established that if we are given a nondeterministicBüchi automaton A that specifies the “bad traces” (i.e., that accepts the complementof the LT property P to be verified), then a graph analysis in the product of the giventransition system TS and the automaton A suffices to either establish or disprove TS |= P .Whereas for regular safety properties a reduction to invariant checking (i.e., a depth-firstsearch) is possible, the graph algorithms needed here serve to check a so-called persistenceproperty. Such properties state that eventually for ever a certain proposition holds.We first introduce the “ω-counterpart” to regular languages, both by introducing ω-regularexpressions (Section 4.3.1) and nondeterministic Büchi automata (see Section 4.3.2).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
