5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 44

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 44)

Thenq 0 ∈ Q0andL(s )iqi −−−−→ qi+1for all i 0.Furthermore, qi ∈ F for infinitely many indices i. Thus, we can combine π and the runq0 q1 . . . to obtain a path in the productπ = s0 , q1 s1 , q2 . . . ∈ Paths(TS ⊗ A).202Regular Properties{ red }{ green }trueq0¬green¬greenq1truegreen{ q0 }{ q1 }{ q2 }s0 , q0 s0 , q1 s0 , q2 s1 , q0 s1 , q1 s1 , q2 { q0 }{ q1 }{ q2 }q2Figure 4.22: A simple traffic light (upper left), an NBA corresponding to Ppers (upperright), and their product (below).Since qi ∈ F for infinitely many i, we have π |= Ppers(A) .

This yields TS ⊗ A |= Ppers(A) .Example 4.64.Checking a Persistence PropertyConsider a simple traffic light as one typically encounters at pedestrian crossings. It onlyhas two possible modes: red or green. Assume that the traffic light is initially red, andalternates between red and green, see the transition system PedTrLight depicted in theupper left part of Figure 4.22. The ω-regular property P to be checked is “infinitely oftengreen”. The complement property P thus is “eventually always not green”. The NBAdepicted in the upper right part of Figure 4.22 accepts P .To check the validity of P , we first construct the product automaton PedTrLight ⊗ A, seethe lower part of Figure 4.22.

Note that the state s1 , q1 is unreachable and could beomitted. Let Ppers (A) = “eventually forever ¬q1 ”. From the lower part of Figure 4.22 onecan immediately infer that there is no run of the product automaton that goes infinitelyoften through a state of the form ·, q1 . That is, transition system PedTrLight and NBAA do not have any trace in common. Thus we conclude:PedTrLight ⊗ A |= “eventually forever” ¬q1and consequently (as expected):PedTrLight |= “infinitely often green”.Model-Checking ω-Regular Properties203As a slight alternative, we now consider a pedestrian traffic light that may automaticallyswitch off to save energy.

Assume, for simplicity, that the light may only switch off whenit is red for some undefined amount of time. Clearly, this traffic light cannot guaranteethe validity of P = “eventually forever ¬green” as it exhibits a run that (possibly aftera while) alternates between red and off infinitely often. This can be formally shown asfollows. First, we construct the product automaton, see Figure 4.23 (lower part). Forinstance, the path s0 , q0 (s2 , q1 s0 , q1 )ω goes infinitely often through the accept stateq1 of A and generates the trace{ red } ∅ { red } ∅ { red } ∅ . .

. . . .That is, Traces(PedTrLight’) ∩ Lω (A) = ∅, and thusPedTrLight’ ⊗ A |= “eventually forever” ¬q1and thusPedTrLight |= “infinitely often green”.More concretely, the path π = s0 s1 s0 s1 . . . generating the tracetrace(π) = { red } ∅ { red } ∅ { red } ∅ . .

.has an accepting run q0 (q1 )ω in A.According to Theorem 4.63, the problem of checking an arbitrary ω-regular property canbe solved with algorithms that check a simple type of ω-regular liveness property, namelypersistence properties. An algorithm for the latter will be provided in the following sectionwhere the transition system under consideration results from the product of the originaltransition system and an NBA for the undesired behaviors.4.4.2Nested Depth-First SearchThe next problem that we need to tackle is how to establish whether for a given finitetransition system TS:TS |= Pperswhere Ppers is a persistence property. Let Φ be the underlying propositional formula thatspecifies the state condition which has to hold ”eventually forever”.The following result shows that answering the question ”does TS |= Ppers hold?” amountsto checking whether TS contains a reachable state violating Φ that is on a cycle in TS.204Regular Properties∅{ red }{ green }s2s0s1{ q0 }{ q1 }{ q2 }s2 , q0 s2 , q1 s2 , q2 s0 , q0 { q0 }s0 , q1 { q1 }s0 , q2 { q2 }s1 , q0 s1 , q1 s1 , q2 { q0 }{ q1 }{ q2 }Figure 4.23: A simple traffic light that can switch off (upper part) and its product (lowerpart).Model-Checking ω-Regular Properties205Φ∈ Q0Φ¬ΦΦΦΦsΦ¬ΦΦFigure 4.24: An example of a run violating “eventually always” Φ.This can be justified intuitively as follows.

Suppose s is a state that is reachable from aninitial state in TS and s |= Φ. As s is reachable, TS has an initial path fragment thatends in s. If s is on a cycle, then this path fragment can be continued by an infinitepath that is obtained by traversing the cycle containing s infinitely often. In this way,we obtain a path in TS that visits the ¬Φ-state s infinitely often. But then, TS |= Ppers .This is exemplified in Figure 4.24 where a fragment of a transition system is shown; forsimplicity the action labels have been omitted. (Note that – in contrast to invariants – astate violating Φ which is not on a cycle does not cause the violation of Ppers .)The reduction of checking whether TS |= Ppers to a cycle detection problem is formalizedby the following theorem.Theorem 4.65.Persistence Checking and Cycle DetectionLet TS be a finite transition system without terminal states over AP, Φ a propositionalformula over AP, and Ppers the persistence property ”eventually forever Φ”.

Then, thefollowing statements are equivalent:(a) TS |= Ppers ,(b) There exists a reachable ¬Φ-state s which belongs to a cycle. Formally:∃s ∈ Reach(TS). s |= Φ ∧ s is on a cycle in G(TS) .5Before providing the proof, let us first explain how to obtain an error indication whenever = u0 u1 u2 . . .

uk be a path in the graph induced by TS, i.e., G(TS),TS |= Ppers . Let π is a cycle in G(TS) containingsuch that k > 0 and s = u0 = uk . Assume s |= Φ. That is, π5Recall that G(TS) denotes the underlying directed graph of TS.206Regular Propertiesa state violating Φ. Let s0 s1 s2 .

. . sn be an initial path fragment of TS such that sn = s.Then the concatenation of this initial path fragment and the unfolding of the cycleπ = s0 s1 s2 . . . sn u1 u2 . . . uk u1 u2 . . . uk . . .=s=s=sis a path in TS. As state s |= Φ is visited by π infinitely often, it follows that π does notsatisfy “eventually always Φ”. The prefixs0 s1 s2 .

. . sn u1 u2 . . . uk=s=scan be used as diagnostic feedback as it shows that s may be visited infinitely often.Proof: Let TS = (S, Act, →, I, AP).(a) =⇒ (b): Assume TS |= Ppers , i.e., there exists a path π = s0 s1 s2 . . . in TS such thattrace(π) ∈/ Ppers . Thus, there are infinitely many indices i such that si |= Φ. Since TS isfinite, there is a state s with s = si |= Φ for infinitely many i. As s appears on a pathstarting in an initial state we have s ∈ Reach(TS). A cycle π is obtained by any fragmentsi si+1 si+2 . . . si+k of π where si = si+k = s and k > 0.

is(b) =⇒ (a): Let s and π = u0 u1 . . . uk be as indicated above, i.e., s ∈ Reach(TS) and πa cycle in TS with s = u0 = uk . Since s ∈ Reach(TS), there in an initial state s0 ∈ I anda path fragment s0 s1 . . . sn with sn = s. Then:π = s0 s1 s2 . . . sn u1 u2 . . . uk u1 u2 uk . . .=s=s=sis a path in TS. Since s |= Φ, it follows that π does not satisfy “eventually forever Φ”,and thus TS |= Ppers .Example 4.66.Pedestrian Traffic Lights RevisitedConsider the transition system model of the simple traffic light that one typically encounters at pedestrian crossings (see Figure 4.22) and the persistence property “eventuallyforever” ¬q1 where q1 is the accept state of the NBA A. As there is no reachable cycle inthe product transition system that contains a state violating ¬q1 , i.e., a cycle that containsa state labeled with q1 , it follows thatPedTrLight ⊗ A |= “eventually forever” ¬q1 .For the traffic light that has the possibility to automatically switch off, it can be inferreddirectly from the product transition system (see the lower part of Figure 4.23) that thereModel-Checking ω-Regular Properties207is a reachable state, e.g., s2 , q1 |= ¬q1 , that lies on a cycle.

Thus:PedTrLight’ ⊗ A |= “eventually forever” ¬q1 .Thus, persistence checking for a finite transition system requires the same techniques aschecking emptiness of an NBA, see page 184. In fact, the algorithm we suggest below canalso be used for checking emptiness in an NBA.A Naive Depth-First Search Theorem 4.65 entails that in order to check the validityof a persistence property, it suffices to check whether there exists a reachable cycle containing a ¬Φ-state.

Характеристики

Список файлов книги