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

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

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

Hence, the additional space complexity of invariant checking islinear in the number of reachable states.Theorem 3.21.Time Complexity of Invariant CheckingThe time complexity of Algorithm 4 is O( N ∗ (1 + |Φ|) + M ) where N denotes the numberof reachable states, and M = s∈S |Post(s)| the number of transitions in the reachablefragment of TS.Proof: The time complexity of the forward reachability on the state graph G(TS) isO(N + M ). The time needed to check s |= Φ for some state s is linear in the lengthof Φ.6 As for each state s it is checked whether Φ holds, this amounts to a total ofN + M + N ∗ (1 + |Φ|) operations.3.3.2Safety PropertiesAs we have seen in the previous section, invariants can be viewed as state properties andcan be checked by considering the reachable states. Some safety properties, however, mayimpose requirements on finite path fragments, and cannot be verified by considering thereachable states only.

To see this, consider the example of a cash dispenser, also knownas an automated teller machine (ATM). A natural requirement is that money can only bewithdrawn from the dispenser once a correct personal identifier (PIN) has been provided.This property is not an invariant, since it is not a state property. It is, however, consideredTo cover the special case where Φ is an atomic proposition, in which case |Φ| = 0, we deal with 1 + |Φ|for the cost to check whether Φ holds for a given state s.6112Linear-Time Propertiesto be a safety property, as any infinite run violating the requirement has a finite prefixthat is “bad”, i.e., in which money is withdrawn without issuing a PIN before.Formally, safety property P is defined as an LT property over AP such that any infiniteword σ where P does not hold contains a bad prefix. The latter means a finite prefix σwhere the bad thing has happened, and thus no infinite word that starts with this prefixσ fulfills P .Definition 3.22.Safety Properties, Bad PrefixesAn LT property Psafe over AP is called a safety property if for all words σ ∈ (2AP )ω \ Psafethere exists a finite prefix σ of σ such that is a finite prefix of σ = ∅.Psafe ∩ σ ∈ (2AP )ω | σAny such finite word σ is called a bad prefix for Psafe .

A minimal bad prefix for Psafedenotes a bad prefix σ for Psafe for which no proper prefix of σ is a bad prefix for Psafe .In other words, minimal bad prefixes are bad prefixes of minimal length. The set of allbad prefixes for Psafe is denoted by BadPref(Psafe ), the set of all minimal bad prefixes byMinBadPref(Psafe ).Let us first observe that any invariant is a safety property.

For propositional formula Φover AP and its invariant Pinv , all finite words of the formA0 A1 . . . An ∈ (2AP )+with A0 |= Φ, . . . , An−1 |= Φ and An |= Φ constitute the minimal bad prefixes forPinv . The following two examples illustrate that there are safety properties that are notinvariants.Example 3.23.A Safety Property for a Traffic LightWe consider a specification of a traffic light with the usual three phases “red”, “green”,and “yellow”. The requirement that each red phase should be immediately preceded by ayellow phase is a safety property but not an invariant.

This is shown in the following.Let red, yellow, and green be atomic propositions. Intuitively, they serve to mark thestates describing a red (yellow or green) phase. The property “always at least one of thelights is on” is specified by:{ σ = A0 A1 . . . | Aj ⊆ AP ∧ Aj = ∅ }.The bad prefixes are finite words that contain ∅. A minimal bad prefix ends with ∅. Theproperty “it is never the case that two lights are switched on at the same time” is specifiedSafety Properties and Invariants113by{ σ = A0 A1 . . . | Aj ⊆ AP ∧ |Aj | 1 }.Bad prefixes for this property are words containing sets such as { red, green }, { red, yellow },and so on. Minimal bad prefixes end with such sets.Now let AP = { red, yellow }.

The property “a red phase must be preceded immediatelyby a yellow phase” is specified by the set of infinite 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. An example of bad prefixesthat are minimal is:∅ ∅ { red } and ∅ { red }.The following bad prefix is not minimal:{ yellow } { yellow } { red } { red } ∅ { red }since it has a proper prefix { yellow } { yellow } { red } { red } which is also a bad prefix.The minimal bad prefixes of this safety property are regular in the sense that they constitute a regular language. The finite automaton in Figure 3.9 accepts precisely the minimalbad prefixes for the above safety property.7 Here, ¬yellow should be read as either ∅ or{ red }.

Note the other properties given in this example are also regular.s1yellow¬yellowyellows0reds2∅Figure 3.9: A finite automaton for the minimal bad prefixes of a regular safety property.Example 3.24.A Safety Property for a Beverage Vending MachineFor a beverage vending machine, a natural requirement is that“The number of inserted coins is always at least the number of dispensed drinks.”7The main concepts of a finite automaton as acceptors for languages over finite words are summarizedin Section 4.1.114Linear-Time PropertiesUsing the set of propositions { pay, drink } and the obvious labeling function, this propertycould be formalized by the set of infinite words A0 A1 A2 .

. . such that for all i 0 we have| { 0 j i | pay ∈ Aj } | |{ 0 j i | drink ∈ Aj } |Bad prefixes for this safety property are, for example∅ { pay } { drink } { drink }and∅ { pay } { drink } ∅ { pay } { drink } { drink }It is left to the interested reader to check that both beverage vending machines fromFigure 3.8 satisfy the above safety property.Safety properties are requirements for the finite traces which is formally stated in thefollowing lemma:Lemma 3.25.Satisfaction Relation for Safety PropertiesFor transition system TS without terminal states and safety property Psafe :TS |= Psafe if and only if Tracesfin (TS) ∩ BadPref(Psafe ) = ∅.Proof: ”if”: By contradiction. Let Tracesfin (TS) ∩ BadPref(Psafe ) = ∅ and assume that/ Psafe for some path π in TS.

Thus, trace(π) starts with aTS |= Psafe . Then, trace(π) ∈ ∈ Tracesfin (TS) ∩ BadPref(Psafe ). Contradiction.bad prefix σ for Psafe . But then, σ ∈ Tracesfin (TS) ∩”only if”: By contradiction. Let TS |= Psafe and assume that σ = A1 . . . An ∈ Tracesfin (TS) can be extended to anBadPref(Psafe ). The finite trace σ/ Psafe and thus,infinite trace σ = A1 .

. . An An+1 An+2 . . . ∈ Traces(TS). Then, σ ∈TS |= Psafe .We conclude this section with an alternative characterization of safety properties by meansof their closure.Definition 3.26.For trace σ ∈Prefix and Closure(2AP )ω ,let pref(σ) denote the set of finite prefixes of σ, i.e., is a finite prefix of σ }.pref(σ) = { σ ∈ (2AP )∗ | σSafety Properties and Invariants115that is, if σ = A0 A1 . . .

then pref(σ) = {ε, A0 , A0 A1 , A0 A1 A2 , . . . } is an infinite set offinite words. This notion is lifted to sets of traces in the usual way. For property P overAP:pref(σ).pref(P ) =σ∈PThe closure of LT property P is defined byclosure(P ) = {σ ∈ (2AP )ω | pref(σ) ⊆ pref(P )}.For instance, for infinite trace σ = ABABAB . . .

(where A, B ⊆ AP) we have pref(σ) ={ ε, A, AB, ABA, ABAB, . . . } which equals the regular language given by the regular expression (AB)∗ (A + ε).The closure of an LT property P is the set of infinite traces whose finite prefixes are alsoprefixes of P . Stated differently, infinite traces in the closure of P do not have a prefixthat is not a prefix of P itself. As we will see below, the closure is a key concept in thecharacterization of safety and liveness properties.Lemma 3.27.Alternative Characterization of Safety PropertiesLet P be an LT property over AP. Then, P is a safety property iff closure(P ) = P .Proof: “if”: Let us assume that closure(P ) = P . To show that P is a safety property,we take an element σ ∈ (2AP )ω \ P and show that σ starts with a bad prefix for P .

Sinceσ∈/ P = closure(P ) there exists a finite prefix σ of σ with σ∈/ pref(P ). By definition of ∈ pref(σ ) belongs to P . Hence, σ is apref(P ), none of the words σ ∈ (2AP )ω where σbad prefix for P , and by definition, P is a safety property.“only if”: Let us assume that P is a safety property. We have to show that P =closure(P ). The inclusion P ⊆ closure(P ) holds for all LT properties. It remains toshow that closure(P ) ⊆ P . We do so by contradiction.

Let us assume that there is someσ = A1 A2 . . . ∈ closure(P ) \ P . Since P is a safety property and σ ∈ P , σ has a finiteprefixσ = A1 . . . An ∈ BadPref(P ).As σ ∈ closure(P ) we have σ ∈ pref(σ) ⊆ pref(P ). Hence, there exists a word σ ∈ P ofthe formσ = A1 . . . An Bn+1 Bn+2 . . . bad prefixThis contradicts the fact that P is a safety property.1163.3.3Linear-Time PropertiesTrace Equivalence and Safety PropertiesWe have seen before that there is a strong relationship between trace inclusion of transitionsystems and the satisfaction of LT properties (see Theorem 3.15, page 104):Traces(TS) ⊆ Traces(TS )if and only iffor all LT properties P :TS |= P implies TS |= Pfor transition systems TS and TS without terminal states.

Note that this result considersall infinite traces. The above thus states a relationship between infinite traces of transitionsystems and the validity of LT properties. When considering only finite traces instead ofinfinite ones, a similar connection with the validity of safety properties can be established,as stated by the following theorem.Theorem 3.28.Finite Trace Inclusion and Safety PropertiesLet TS and TS be transition systems without terminal states and with the same set ofpropositions AP.

Then the following statements are equivalent:(a) Tracesfin (TS) ⊆ Tracesfin (TS ),(b) For any safety property Psafe : TS |= Psafe implies TS |= Psafe .Proof:(a) =⇒ (b): Let us assume that Tracesfin (TS) ⊆ Tracesfin (TS ) and let Psafe be a safetyproperty with TS |= Psafe . By Lemma 3.25, we have Tracesfin (TS ) ∩ BadPref(Psafe ) = ∅,and hence, Tracesfin (TS)∩ BadPref(Psafe ) = ∅. Again by Lemma 3.25, we get TS |= Psafe .(b) =⇒ (a): Assume that (b) holds. Let Psafe = closure(Traces(TS )). Then, Psafe is asafety property and we have TS |= Psafe (see Exercise 3.9, page 147).

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

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