5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 25
Текст из файла (страница 25)
Then:Traces(TS) = Traces(TS )⇐⇒TS and TS satisfy the same LT properties.There thus does not exist an LT property that can distinguish between trace-equivalenttransition systems. Stated differently, in order to establish that the transition systems TSand TS are not trace-equivalent it suffices to find one LT property that holds for one butnot for the other.Example 3.19.Two Beverage Vending MachinesConsider the two transition systems in Figure 3.8 that both model a beverage vendingpaypayττsodaτselectτbeerselect1sodabeerselect2Figure 3.8: Two beverage vending machines.machine. For simplicity, the observable action labels of transitions have been omitted.Both machines are able to offer soda and beer.
The left transition system models abeverage machine that after insertion of a coin nondeterministically chooses to eitherprovide soda or beer. The right one, however, has two selection buttons (one for eachbeverage), and after insertion of a coin, nondeterministically blocks one of the buttons. Ineither case, the user has no control over the beverage obtained—the choice of beverage isunder full control of the vending machine.Let AP = { pay , soda, beer }.
Although the two vending machines behave differently, itis not difficult to see that they exhibit the same traces when considering AP, as for bothmachines traces are alternating sequences of pay and either soda or beer. The vendingmachines are thus trace-equivalent. By Corollary 3.18 both vending machines satisfyexactly the same LT properties. Stated differently, it means that there does not exist anLT property that distinguishes between the two vending machines.Safety Properties and Invariants3.3107Safety Properties and InvariantsSafety properties are often characterized as “nothing bad should happen”.
The mutualexclusion property—always at most one process is in its critical section—is a typical safetyproperty. It states that the bad thing (having two or more processes in their critical sectionsimultaneously) never occurs. Another typical safety property is deadlock freedom. Forthe dining philosophers (see Example 3.2, page 90), for example, such deadlock could becharacterized as the situation in which all philosophers are waiting to pick up the secondchopstick.
This bad (i.e., unwanted) situation should never occur.3.3.1InvariantsIn fact, the above safety properties are of a particular kind: they are invariants. Invariantsare LT properties that are given by a condition Φ for the states and require that Φ holdsfor all reachable states.Definition 3.20.InvariantAn LT property Pinv over AP is an invariant if there is a propositional logic formula5 Φover AP such thatPinv = A0 A1 A2 .
. . ∈ (2AP )ω | ∀j 0. Aj |= Φ .Φ is called an invariant condition (or state condition) of Pinv .Note thatTS |= Pinviffiffifftrace(π) ∈ Pinv for all paths π in TSL(s) |= Φ for all states s that belong to a path of TSL(s) |= Φ for all states s ∈ Reach(TS).Thus, the notion ”invariant” can be explained as follows: the condition Φ has to be fulfilledby all initial states and satisfaction of Φ is invariant under all transitions in the reachablefragment of the given transition system. The latter means that if Φ holds for the sourceas , then Φ holds for the target state s too.state s of a transition s −→Let us return to the examples of mutual exclusion and deadlock freedom for the diningphilosophers. The mutual exclusion property can be described by an invariant using the5The basic principles of propositional logic are treated in Appendix A.3.108Linear-Time Propertiespropositional logic formulaΦ = ¬crit1 ∨ ¬crit2 .For deadlock freedom of the dining philosophers, the invariant ensures that at least oneof the philosophers is not waiting to pick up the chopstick.
This can be established usingthe propositional formula:Φ = ¬wait0 ∨ ¬wait1 ∨ ¬wait2 ∨ ¬wait3 ∨ ¬wait4 .Here, the proposition waiti characterizes the state(s) of philosopher i in which he is waitingfor a chopstick.How do we check whether a transition system satisfies an invariant? As checking aninvariant for the propositional formula Φ amounts to checking the validity of Φ in everystate that is reachable from some initial state, a slight modification of standard graphtraversal algorithms like depth-first search (DFS) or breadth-first search (BFS) will do,provided the given transition system TS is finite.Algorithm 3 on page 109 summarizes the main steps for checking the invariant conditionΦ by means of a forward depth-first search in the state graph G(TS).
The notion forward search means that we start from the initial states and investigate all states that arereachable from them. If at least one state s is visited where Φ does not hold, then theinvariance induced by Φ is violated. In Algorithm 3, R stores all visited states, i.e., ifAlgorithm 3 terminates, then R = Reach(TS) contains all reachable states. Furthermore,U is a stack that organizes all states that still have to be visited, provided they are notyet contained in R. The operations push, pop, and top are the standard operations onstacks. The symbol ε is used to denote the empty stack.
Alternatively, a backward searchcould have been applied that starts with∗all states where Φ does not hold and calculates(by a DFS or BFS) the set s∈S,s|=Φ Pre (s).Algorithm 3 could be slightly improved by aborting the computation once a state s isencountered that does not fulfill Φ. This state is a “bad” state as it makes the transitionsystem refute the invariant and could be returned as an error indication. Such errorindication, however, is not very helpful.Instead, an initial path fragment s0 s1 s2 . . . sn in which all states (except the last one)satisfy Φ and sn |= Φ would be more useful. Such a path fragment indicates a possiblebehavior of the transition system that violates the invariant.
Algorithm 3 can be easilyadapted such that a counterexample is provided on encountering a state that violatesΦ. To that end we exploit the (depth-first search) stack U . When encountering sn thatviolates Φ, the stack content, read from bottom to top, contains the required initial pathfragment. Algorithm 4 on page 110 thus results.Safety Properties and Invariants109Algorithm 3 Naı̈ve invariant checking by forward depth-first searchInput: finite transition system TS and propositional formula ΦOutput: true if TS satisfies the invariant ”always Φ”, otherwise falseset of state R := ∅;stack of state U := ε;bool b := true;for all s ∈ I doif s ∈/ R thenvisit(s)fiodreturn bprocedure visit (state s)push(s, U );R := R ∪ { s };repeats := top(U );if Post(s ) ⊆ R thenpop(U );b := b ∧ (s |= Φ);elselet s ∈ Post(s ) \ Rpush(s , U );R := R ∪ { s };fiuntil (U = ε)endproc(* the set of visited states *)(* the empty stack *)(* all states in R satisfy Φ *)(* perform a dfs for each unvisited initial state *)(* push s on the stack *)(* mark s as reachable *)(* check validity of Φ in s *)(* state s is a new reachable state *)110Linear-Time PropertiesAlgorithm 4 Invariant checking by forward depth-first searchInput: finite transition system TS and propositional formula ΦOutput: ”yes” if TS |= ”always Φ”, otherwise ”no” plus a counterexampleset of states R := ∅;stack of states U := ε;bool b := true;while (I \ R = ∅ ∧ b) dolet s ∈ I \ R;visit(s);odif b thenreturn(”yes”)elsereturn(”no”, reverse(U ))fiprocedure visit (state s)push(s, U );R := R ∪ { s };repeats := top(U );if Post(s ) ⊆ R thenpop(U );b := b ∧ (s |= Φ);elselet s ∈ Post(s ) \ Rpush(s , U );R := R ∪ { s };fiuntil ((U = ε) ∨ ¬ b)endproc(* the set of reachable states *)(* the empty stack *)(* all states in R satisfy Φ *)(* choose an arbitrary initial state not in R *)(* perform a DFS for each unvisited initial state *)(* TS |= ”always Φ” *)(* counterexample arises from the stack content *)(* push s on the stack *)(* mark s as reachable *)(* check validity of Φ in s *)(* state s is a new reachable state *)Safety Properties and Invariants111The worst-case time complexity of the proposed invariance checking algorithm is dominated by the cost for the DFS that visits all reachable states.
The latter is linear in thenumber of states (nodes of the state graph) and transitions (edges in the state graph),provided we are given a representation of the state graph where the direct successorss ∈ Post(s) for any state s can be encountered in time Θ(|Post(s)|). This holds for arepresentation of the sets Post(s) by adjacency lists. An explicit representation of adjacency lists is not adequate in our context where the state graph of a complex system hasto be analyzed. Instead, the adjacency lists are typically given in an implicit way, e.g.,by a syntactic description of the concurrent processes, such as program graphs or higherlevel description languages with a program graph semantics such as nanoPromela, seeSection 2.2.5, page 63).
The direct successors of a state s are then obtained by the axiomsand rules for the transition relation for the composite system. Besides the space for thesyntactic descriptions of the processes, the space required by Algorithm 4 is dominated bythe representation of the set R of visited states (this is typically done by appropriate hashtechniques) and stack U .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
