5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 36
Текст из файла (страница 36)
Itmust be distinguished from the regular expression ∅ representing the empty language.1160Regular Properties• Φ stands for the regular expression {} + { a } + { a, b },• ¬Φ stands for the regular expression consisting of the symbol { b },• true stands for the regular expression {} + { a } + { b } + { a, b }.The bad prefixes of the invariant over condition a ∨ ¬b are given by the regular expression:E = ({} + { a } + { a, b })∗ { b } ({} + { a } + { b } + { a, b })∗ . Φ∗true∗¬ΦThus, L(E) consists of all words A1 . .
. An such that Ai = { b } for some 1 i n. Notethat, for A ⊆ AP = { a, b }, we have A |= a ∨ ¬b if and only if A = { b }. Hence, L(E)agrees with the set of bad prefixes for the invariant induced by the condition Φ.¬Φq0q1trueΦFigure 4.3: NFA accepting all bad prefixes of the invariant over the condition Φ.In fact, for any invariant Pinv , the language of all bad prefixes can be represented by anNFA with two states, as shown in Figure 4.3. Here and in the sequel, we use symbolicnotations in the pictures for NFAs over the alphabet 2AP .
We use propositional formulaeover AP as labels for the edges. Thus, an edge leading from state q to state q labeledA → q for all A ⊆ AP where A |= Ψ.with formula Ψ means that there are transitions q −−E.g., if AP = { a, b } and Φ = a ∨ ¬b, then Figure 4.3 is a representation for an NFA withtwo states q0 , q1 and the transitions{}{a}{a,b}{}{a}{b}{b}q0 −−→ q0 , q0 −−−→ q0 , q0 −−−−→ q0 , q0 −−−→ q1and{a,b}q1 −−→ q1 , q1 −−−→ q1 , q1 −−−→ q1 , q1 −−−−→ q1 .For the invariant over AP = { a, b } induced by the condition Φ = a ∨ ¬b, the minimalbad prefixes are described by the regular expression ({} + { a } + { a, b })∗ { b }. Hence, theminimal bad prefixes constitute a regular language too. An automaton that recognizes allminimal bad prefixes, which are given by the regular expression Φ∗ (¬Φ), is obtained fromFigure 4.3 by omitting the self-loop of state q1 .
In fact, for the definition of regular safetyproperties it is irrelevant whether the regularity of the set of all bad prefixes or of the setof all minimal bad prefixes is required:Model-Checking Regular Safety PropertiesLemma 4.12.161Criterion for Regularity of Safety PropertiesThe safety property Psafe is regular if and only if the set of minimal bad prefixes for Psafeis regular.Proof: “if”: Let A = (Q, 2AP , δ, Q0 , F ) be an NFA for MinBadPref(Psafe ).
Then, anANFA for BadPref(Psafe ) is obtained by adding self-loops q −−→ q for all states q ∈ F andall A ⊆ AP. It is easy to check that the modified NFA accepts the language consisting ofall bad prefixes for Psafe . Thus, BadPref(Psafe ) is regular, which yields the claim.“only if”: Let A = (Q, 2AP , δ, Q0 , F ) be a DFA for BadPref(Psafe ). For MinBadPref(Psafe ),a DFA is obtained by removing all outgoing transitions from the accept states in A.
LetA be the modified DFA and let us check that L(A ) = MinBadPref(Psafe ).If we are given a word w = A1 . . . An ∈ L(A ), then w ∈ L(A) since the run q0 q1 . . . qn inA for w is also an accepting run in A. Therefore, w is a bad prefix for Psafe . Distinguishtwo cases.Assume w is not a minimal bad prefix. Then there exists a proper prefix A1 . . .
Ai of wthat is a bad prefix for Psafe . Thus, A1 . . . Ai ∈ L(A). Since A is deterministic, q0 q1 . . . qiis the (unique) run for A1 . . . Ai in A and qi ∈ F . Since i < n and qi has no outgoingtransitions in A , q0 . . . qi . . . qn cannot be a run for A1 . .
. Ai . . . An in A . This contradictsthe assumption and shows that A1 . . . An is a minimal bad prefix for Psafe .Vice versa, if w is a minimal bad prefix for Psafe , then(1) A1 . . . An ∈ BadPref(Psafe ) = L(A) and/ BadPref(Psafe ) = L(A) for all 1 i < n.(2) A1 . . . Ai ∈/ F for 1 i < n, whileLet q0 . .
. qn be the unique run for w in A. Then, (2) yields qi ∈qn ∈ F by (1). Thus, q0 . . . qn is an accepting run for w in A which yields w ∈ L(A ).Example 4.13.Regular Safety Property for Mutual Exclusion AlgorithmsConsider a mutual exclusion algorithm such as the semaphore-based one or Peterson’salgorithm. The bad prefixes of the safety property Pmutex (“there is always at most oneprocess in its critical section”) constitute the language of all finite words A0 A1 . . . An suchthat{ crit1 , crit2 } ⊆ Ai162Regular Propertiesfor some index i with 0 i n. If i=n is the smallest such index, i.e., { crit1 , crit2 } ⊆ Anand { crit1 , crit2 } ⊆ Aj for 0 j < n, then A0 . .
. An is a minimal bad prefix. Thelanguage of all (minimal) bad prefixes is regular. An NFA recognizing all minimal badprefixes is depicted in Figure 4.4.q0crit1 ∧ crit2q1¬ (crit1 ∧ crit2 )Figure 4.4: Minimal bad prefixes that refute the mutual exclusion property.Example 4.14.Regular Safety Property for the Traffic LightConsider a traffic light with three possible colors: red, yellow and green. The property“a red phase must be preceded immediately by a yellow phase” is specified by the set ofinfinite words σ = A0 A1 .
. . with Ai ⊆ { red, yellow } such that for all i 0 we have thatred ∈ Ai implies i > 0 and yellow ∈ Ai−1 .The bad prefixes are finite words that violate this condition. Examples of bad prefixesthat are minimal are{} {} { red } and {} { red }.In general, the minimal bad prefixes are words of the form A0 A1 . . .
An such that n > 0,red ∈ An , and yellow ∈ An−1 . The NFA in Figure 4.5 accepts these minimal bad prefixes.Recall the meaning of the edge labels in the pictorial representations of an NFA over theq1yellow¬yellow¬red ∧ yellowq0redq2¬red ∧ ¬yellowFigure 4.5: Minimal bad prefixes in which red is not preceded by yellow.alphabet Σ = 2AP where AP = { yellow,red }.
For instance, the edge-label yellow in theself-loop of state q1 denotes a formula, namely the positive literal yellow ∈ AP. Thisstands for all sets A ⊆ AP = { yellow,red } where the literal yellow holds, that is, the sets{ yellow } and { yellow, red }. Hence, the self-loop of q1 in the picture stands for the twoModel-Checking Regular Safety Propertiestransitions:163{yellow}{yellow,red}q1 −−−−−−→ q1 and q1 −−−−−−−−−→ q1 .Similarly, the edge label ¬yellow in the transition from q1 to q0 stands for the negativeliteral ¬yellow, and thus represents the transitions:{red}q1 −−−−→ q0and{}q1 −−→ q0 .In the same way the label red of the transition from q0 to q2 represents two transitions (withthe labels { red } and { red, yellow }), while the edge labels ¬red∧yellow and ¬red∧¬yellowdenote only a single symbol in 2AP , namely { yellow } and {}, respectively.Example 4.15.A Nonregular Safety PropertyNot all safety properties are regular.
As an example of a nonregular safety property,consider:“The number of inserted coins is always at least the number of dispensed drinks.”(See also Example 3.24 on page 113). Let the set of propositions be { pay, drink }. Minimalbad prefixes for this safety property constitute the language{ payn drinkn+1 | n 0 }which is not a regular, but a context-free language. Such safety properties fall outside thescope of the following verification algorithm.4.2.2Verifying Regular Safety PropertiesLet Psafe be a regular safety property over the atomic propositions AP and A an NFArecognizing the (minimal) bad prefixes of Psafe . (Recall that by Lemma 4.12 on page 161it is irrelevant whether A accepts all bad prefixes for Psafe or only the minimal ones.) Fortechnical reasons, we assume that ε ∈/ L(A).
In fact, this is not a severe restriction sinceAPare bad prefixes, and hence, Psafe = ∅. In this case,otherwise all finite words over 2TS |= Psafe if and only if TS has no initial state.Furthermore, let TS be a finite transition system without terminal states with corresponding set of propositions AP.
In this section, we aim to establish an algorithmic methodfor verifying whether TS satisfies regular safety property Psafe , i.e., to check whether164Regular PropertiesTS |= Psafe holds. According to Lemma 3.25 on page 114 we haveTS |= Psafeif and only if Tracesfin (TS) ∩ BadPref(Psafe ) = ∅if and only if Tracesfin (TS) ∩ L(A) = ∅.Thus, it suffices to check whether Tracesfin (TS) ∩ L(A) = ∅ to establish TS |= Psafe .To do so, we adopt a similar strategy as for checking whether two NFAs intersect. Recallthat in order to check whether the NFAs A1 and A2 do intersect, it suffices to considertheir product automaton, soL(A1 ) ∩ L(A2 ) = ∅if and only ifL(A1 ⊗ A2 ) = ∅.The question whether two automata do intersect is thus reduced to a simple reachabilityproblem in the product automaton.This is now exploited as follows.
In order to check whether Tracesfin (TS) ∩ L(A) = ∅,we first build a product of transition system TS and NFA A in the same vein as thesynchronous product of NFA. This yields the transition system TS⊗ A. For this transitionsystem, an invariant can be given using a propositional logic formula Φ –derived from theaccept states of A– such that Tracesfin (TS)∩L(A) = ∅ if and only if TS⊗A |= “always Φ”.In this way, the verification of a regular safety property is reduced to invariant checking.Recall that for checking invariants, Algorithm 4 (see page 110) can be exploited.We start by formally defining the product between a transition system TS and an NFAA, denoted TS ⊗ A.
Let TS = (S, Act, →, I, AP, L) and A = (Q, 2AP , δ, Q0 , F ) withQ0 ∩ F = ∅. Recall that the alphabet of A consists of sets of atomic proposition in TS.Transition system TS ⊗ A has state space S × Q and a transition relation such that eachpath fragment π = s0 s1 . . . sn in TS can be extended to a path fragments0 , q1 s1 , q2 . . . sn , qn+1 in TS ⊗ A which has an initial state q0 ∈ Q0 for whichL(s )L(s )L(s )L(s )n012→ q1 −−−−→ q2 −−−−→ . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
