5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 43
Текст из файла (страница 43)
Thereby, A ⊆since q0 ∈{ crit1 , crit2 } is arbitrary.Any NBA can be considered as a GNBA by simply replacing the acceptance set F ofthe NBA with the singleton set F = { F } for the corresponding GNBA. Using this fact,together with the result that NBAs are equally expressive as ω-regular languages (seeTheorem 4.32 on page 178), we obtain by Theorem 4.56:Corollary 4.58.GNBA and ω-Regular LanguagesThe class of languages accepted by GNBAs agrees with the class of ω-regular languages.As we have seen before, ω-regular languages are closed under union.
This is immediatefrom the definition of ω-regular expressions and can also simply be proven by means ofAutomata on Infinite Words197crit1q1 , 1crit2q0 , 1truetruetrueq1 , 2q2 , 1truetruecrit2q0 , 2crit1q2 , 2trueFigure 4.21: Example for the transformation of a GNBA into an equivalent NBA.NBA representations (see Lemma 4.33 on page 179). We now use GNBAs to show thatω-regular languages are closed under intersection too.Lemma 4.59.Intersection of GNBAFor GNBA G1 and G2 (both over the alphabet Σ), there exists a GNBA G withLω (G) = Lω (G1 ) ∩ Lω (G2 )and|G| = O(|G1 | · |G2 |).Proof: Let G1 = (Q1 , Σ, δ1 , Q0,1 , F1 ) and G2 = (Q2 , Σ, δ2 , Q0,2 , F2 ) where without loss ofgenerality Q1 ∩ Q2 = ∅.
Let G be the GNBA that results from G1 and G2 by a synchronousproduct construction (as for NFA) and “lifts” the acceptance sets F ∈ F1 ∪F2 to acceptancesets in G. Formally,G = G1 ⊗ G2 = (Q1 × Q2 , Σ, δ, Q0,1 × Q0,2 , F)where the transition relation δ is defined by the ruleAA→1 q1 ∧ q2 −−→2 q2q1 −−A(q1 , q2 ) −−→ (q1 , q2 ).The acceptance condition in G is given byF = {F1 × Q2 | F1 ∈ F1 } ∪ {Q1 × F2 | F2 ∈ F2 }.198Regular PropertiesIt is now easy to verify that G has the desired properties.The same result also holds for union, that is, given two GNBAs G1 and G2 with the samealphabet Σ there is a GNBA G with Lω (G) = Lω (G1 )∪Lω (G2 ) and |G| = O(|G1 |+|G2 |). Theargument is the same as for NBA (Lemma 4.33): we simply may take the disjoint unionof the two GNBAs and decide nondeterministically which of them is chosen to “scan” thegiven input word.Since GNBA yield an alternative characterization of ω-regular languages, we obtain byLemma 4.59:Corollary 4.60.Intersection of ω-Regular LanguagesIf L1 and L2 are ω-regular languages over the alphabet Σ, then so is L1 ∩ L2 .4.4Model-Checking ω-Regular PropertiesThe examples provided in Section 4.3.2 (see page 176 ff.) illustrated that NBAs yield asimple formalism for ω-regular properties.
We now address the question how the automatabased approach for verifying regular safety properties can be generalized for the verificationof ω-regular properties.The starting point is a finite transition system TS = (S, Act, →, I, AP, L) without terminalstates and an ω-regular property P . The aim is to check algorithmically whether TS |= P .As we did for regular safety properties, the verification algorithm we present now attemptsto show that TS |= P by providing a counterexample, i.e., a path π in TS with trace(π) ∈/P .
(If no such path exists, then P holds for TS.) For this, we assume that we are given anautomata-representation of the “bad traces” by means of an NBA A for the complementproperty P = (2AP )ω \ P . The goal is then to check whether Traces(TS) ∩ Lω (A) = ∅.Note that:Traces(TS) ∩ Lω (A) = ∅if and only if Traces(TS) ∩ P = ∅if and only if Traces(TS) ∩ (2AP )ω \ P = ∅if and only if Traces(TS) ⊆ Pif and only if TS |= P.Model-Checking ω-Regular Properties199The reader should notice the similarities with regular safety property checking.
In thatcase, we started with an NFA for the bad prefixes for the given safety property Psafe(the bad behaviors). This can be seen as an automata-representation of the complementproperty Psafe , see Remark 4.31 on page 177. The goal was then to find a finite, initialpath fragment in TS that yields a trace accepted by the NFA, i.e., a bad prefix for Psafe .Let us now address the problem to check whether Traces(TS) ∩ Lω (A) = ∅. For this,we can follow the same pattern as for regular safety properties and construct the productTS ⊗ A which combines paths in TS with the runs in A.
We then perform a graphanalysis in TS ⊗ A to check whether there is a path that visits an accept state of Ainfinitely often, which then yields a counterexample and proves TS |= P . If no such pathin the product exists, i.e., if accept states can be visited at most finitely many times onall paths in the product, then all runs for the traces in TS are nonaccepting, and henceTraces(TS) ∩ Lω (A) = ∅ and thus TS |= PIn the sequel, we will explain these ideas in more detail. For doing so, we first introducethe notion of a persistence property. This is a simple type of LT property that willserve to formalize the condition stating that accept states are only visited finitely manytimes.
The problem of verifying ω-regular properties is then shown to be reducible tothe persistence checking problem. Recall that the problem of verifying regular safetyproperties is reducible to the invariant checking problem, see Section 4.2.4.4.1Persistence Properties and ProductPersistence properties are special types of liveness properties that assert that from somemoment on a certain state condition Φ holds continuously.
Stated in other words, ¬Φ isrequired to hold at most finitely many times. As for invariants, we assume a representationof Φ by a propositional logic formula over AP.Definition 4.61.Persistence PropertyA persistence property over AP is an LT property Ppers ⊆ (2AP )ω “eventually forever Φ”for some propositional logic formula Φ over AP. Formally,∞Ppers = A0 A1 A2 . .
. ∈ (2AP )ω | ∀ j. Aj |= Φ∞where ∀ j is short for ∃i 0. ∀j i. Formula Φ is called a persistence (or state) conditionof Ppers .Intuitively, a persistence property “eventually forever Φ” ensures the tenacity of the state200Regular Propertiesproperty given by the persistence condition Φ. One may say that Φ is an invariant after awhile; i.e., from a certain point on all states satisfy Φ.
The formula “eventually forever Φ”is true for a path if and only if almost all, i.e., all except for finitely many, states satisfythe proposition Φ.Our goal is now to show that the question whether Traces(TS) ∩ Lω (A) = ∅ holds can bereduced to the question whether a certain persistence property holds in the product of TSand A.
The formal definition of the product TS ⊗ A is exactly the same as for an NFA.For completeness, we recall the definition here:Definition 4.62.Product of Transition System and NBALet TS = (S, Act, →, I, AP, L) be a transition system without terminal states and A =(Q, 2AP , δ, Q0 , F ) a nonblocking NBA. Then, TS ⊗ A is the following transition system:TS ⊗ A = (S × Q, Act, → , I , AP , L )where → is the smallest relation defined by the ruleL(t)α→ t ∧ q −−−→ ps −−α s, q −−→ t, pand whereL(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 }.Furthermore, let Ppers(A) be the persistence property over AP = Q given by”eventually forever ¬F ”where ¬F denotes the propositional formula¬q over AP = Q.q∈QWe now turn to the formal proof that the automata-based approach for checking ω-regularproperties relies on checking a persistence property for the product transition system:Theorem 4.63.Verification of ω-Regular PropertiesLet TS be a finite transition system without terminal states over AP and let P be an ωregular property over AP.
Furthermore, let A be a nonblocking NBA with the alphabet2AP and Lω (A) = (2AP )ω \ P . Then, the following statements are equivalent:Model-Checking ω-Regular Properties201(a) TS |= P(b) Traces(TS) ∩ Lω (A) = ∅(c) TS ⊗ A |= Ppers (A)Proof: Let TS = (S, Act, →, I, AP, L) and A = (Q, 2AP , δ, Q0 , F ). The equivalence of (a)and (b) was shown on page 198. Let us now check the equivalence of (b) and (c).
For thiswe showTraces(TS) ∩ Lω (A) = ∅ if and only if TS ⊗ A |= Ppers(A) .”⇐”: Assume TS ⊗ A |= Ppers (A) . Let π = s0 , q1 s1 , q2 . . . be a path in TS ⊗ A suchthatπ |= Ppers(A) .Then there are infinitely many indices i with qi ∈ F . The projection of π to the states inTS yields a path π = s0 s1 s2 . .
. in TS.L(s )0→ q1 . Such a state q0 exists, sinceLet q0 ∈ Q0 be an initial state of A such that q0 −−−−s0 , q1 is an initial state of TS ⊗ A. The state sequence q0 q1 q2 . . . is a run in A for thewordtrace(π) = L(s0 ) L(s1 ) L(s2 ) . . . ∈ Traces(TS).Since there are infinitely many i with qi ∈ F , the run q0 q1 q2 . . .
is accepting. Hence,trace(π) ∈ Lω (A).This yields trace(π) ∈ Traces(TS) ∩ Lω (A), and thus Traces(TS) ∩ Lω (A) = ∅.”⇒”: Assume that Traces(TS) ∩ Lω (A) = ∅. Then there exists a path in TS, sayπ = s0 s1 s2 . . . withtrace(π) = L(s0 ) L(s1 ) L(s2 ) . . . ∈ Lω (A).Let q0 q1 q2 . . . be an accepting run in A for trace(π).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
