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

According to the definition of → itfollows for any B, C ∈ S/ ∼:B → Cif and only if ∃s ∈ B. ∃s ∈ C. s → sBy condition (2) of Definition 7.7, this is equivalent toB → Cif and only if ∀s ∈ B. ∃s ∈ C. s → s .The following two examples show that enormous state-space reductions may be obtainedby considering the bisimulation quotient. In some cases, it even allows obtaining a finitequotient transition system for infinite transition systems.460Equivalences and AbstractionExample 7.12.Many PrintersConsider a system consisting of n printers, each represented as extremely simplified bytwo states, ready and print . The initial state is ready , and once started, each printeralternates between being ready and printing. The entire system is given byTSn = Printer ||| .

. . ||| Printer .n timesAssume the states of TSn are labeled with atomic propositions from the set AP ={ 0, 1, . . . , n }. Intuitively, L(s) denotes the number of printers available in state s, i.e.,which are in the local state ready . The number of states of TSn is exponential in n (it is2n ); for n=3, TSn is depicted in Figure 7.6, where r denotes ready, and p denotes print.The quotient transition system TSn / ∼, however, only contains n+1 states.

For n=3,TSn / ∼ is depicted in Figure 7.7.r, r, r{2} p, r, r{3}r, r, p {2}r, p, r {2}{1}{0}{1}p, p, rp, p, pr, p, pp, r, p{1}Figure 7.6: Transition system TS3 for three independent printers321Figure 7.7: Bisimulation quotient TS3 /∼.0Bisimulation461Example 7.13.The Bakery AlgorithmWe consider a mutual exclusion algorithm, originally proposed by Lamport, which is knownas the Bakery algorithm. Although the principle of the Bakery algorithm allows guaranteeing mutual exclusion for an arbitrary number of processes, we consider the simplersetting with two processes.

Let P1 and P2 be two processes, and x1 and x2 be two sharedvariables that both initially equal zero, see the following program text:Process 1:Process 2:............while true {while true {............n1 :x1 := x2 + 1;n2 :x2 := x1 + 1;w1 :wait until (x2 = 0 ||x1 < x2 ) {w2 :wait until (x1 = 0 || x2 < x1 ) {c1 :. . .

critical section . . .}}c2 :. . . critical section . . .}x1 := 0;x2 := 0;............}These variables are used to resolve a conflict if both processes want to enter the criticalsection. (One might consider the value of a variable as a ticket, i.e., a number thatone typically gets upon entering a bakery. The holder of the lowest number is the nextcustomer to be served.) If process Pi is waiting, and xi < xj or xj =0, then it may enterthe critical section. We have xi > 0 whenever process Pi is either waiting to acquire accessto the critical section, or is in the critical section. On requesting access to the criticalsection, process Pi sets xi to xj +1, where i = j.

Intuitively, process Pi gives priority toits opponent, process Pj .As the value of x1 and x2 may grow unboundedly, the underlying transition system ofthe parallel composition of P1 and P2 is infinite; a fragment of the transition system isdepicted in Figure 7.8. An example of a path fragment that visits infinitely many differentstates is:462Equivalences and Abstractionprocess P1noncrit1wait1wait1crit1noncrit1wait1wait1wait1wait1...process P2noncrit2noncrit2wait2wait2wait2wait2crit2noncrit2wait2...x1011103333..x2002222204..effectP1 requests access to criticalP2 requests access to criticalP1 enters the critical sectionP1 leaves the critical sectionP1 requests access to criticalP2 enters the critical sectionP2 leaves the critical sectionP2 requests access to criticalP2 enters the critical section...sectionsectionsectionsectionAlthough algorithmic analysis, such as LTL model checking, is impossible due to theinfinity of the transition system, it is not difficult to check that the Bakery algorithmsuffers neither from deadlock nor starvation:• A deadlock only occurs whenever none of the processes can enter the critical section,i.e., if x1 =x2 > 0.

It is easy to see, however, that apart from the initial situation,we always have x1 = x2 .• Starvation only occurs if a process that wants to enter the critical section is neverable to do so. Such situation, however, can never occur: in case both processes wantto enter the critical section, it is impossible that a process acquires access to thecritical section twice in a row.Alternatively, the correctness of the Bakery algorithm can also be established algorithmically.

This is done by considering an abstraction of the infinite transition system suchthat, instead of the concrete values of x1 and x2 , it is only recorded whetherx1 > x2 > 0orx2 > x1 > 0 orx1 = 0 orx2 = 0Note that this information is sufficient to determine which process may acquire accessto the critical section. By means of this data abstraction, we obtain a finite transition, e.g., the infinite set of states for which x1 and x2 exceed 0 is mappedsystem TSabstractBakonto the single abstract state wait1 , wait2 , x1 > x2 > 0. When considering the atomicpropositions{ noncriti , waiti , criti | i = 1, 2 } ∪ { x1 > x2 > 0, x2 > x1 > 0, x1 = 0, x2 = 0 }(with the obvious state labeling) is trace-equivalentthe finite transition system TSabstractBakto the original infinite transition system TSBak .

Due to the fact that trace-equivalenttransition systems satisfy the same LT properties, it follows that each LT property that isBisimulation463shown to hold for the finite (abstract) transition system also holds for the original infinitetransition system! The following LT properties, expressed as LTL formulae, indeed hold:for TSabstractBak(¬crit1 ∨ ¬crit2 ) and( ♦ wait1 ⇒ ♦ crit1 ) ∧ ( ♦ wait2 ⇒ ♦ crit2 ) .n1 c2x1 0x2 1n1 n2x1 0x2 0c1 n2x1 1x2 0n1 w2x1 0x2 1w1 n2x1 1x2 0w1 w2x1 2x2 1n1 c2x1 0x2 2w1 w2x1 1x2 2c1 w2x1 1x2 2n1 w2x1 0x2 2w1 c2x1 2x2 1w1 w2x1 3x2 2n1 c2x1 0x2 3n1 w2c1 n2x1 2x2 0w1 n2x1 2x2 0w1 w2x1 2x2 3c1 w2w1 c2c1 n2x1 3x2 0w1 n2Figure 7.8: Fragment of the infinite transition system of the Bakery algorithm.are bisimilar.

This can be easily proven by inTransition systems TSBak and TSabstractBakdicating a bisimulation relation. The data abstraction described above is formalized bymeans of the function f : S → S where S and S denote the set of reachable states of, respectively. The function f associates to any reachable state s ofTSBak and TSabstractBak. Let s = 1 , 2 , x1 = b1 , x2 = b2 be a stateTSBak , an (abstract) state f (s) of TSabstractBakof TSBak with i ∈ { noncriti , waiti , criti } and bi ∈ IN for i = 1, 2.

Then, we define⎧⎪⎪ 1 , 2 , x1 = 0, x2 = 0 if b1 = b2 = 0⎪⎪⎨ 1 , 2 , x1 = 0, x2 > 0 if b1 = 0 and b2 > 01 , 2 , x1 > 0, x2 = 0 if b1 > 0 and b2 = 0f (s) =⎪⎪if b1 > b2 > 0⎪ 1 , 2 , x1 > x2 > 0⎪⎩if b2 > b1 > 0 .1 , 2 , x2 > x1 > 0464Equivalences and Abstractionn1 n2x1 = 0x2 = 0n1 w2x1 = 0x2 > 0w1 n2x1 > 0x2 = 0n1 c2x1 = 0x2 > 0c1 n2x1 > 0x2 = 0w1 w2x1 > x2 > 0w1 w2x2 > x1 > 0c1 w2x2 > x1 > 0w1 c2x1 > x2 > 0Figure 7.9: Bisimulation quotient transition system of the Bakery algorithmIt follows by straightforward reasoning that R = { (s, f (s)) | s ∈ S } is a bisimulation) for any subset of AP = { noncriti , waiti , criti | i = 1, 2 }.

Thefor (TSBak , TSabstractBakin Figure 7.9 above is the bisimulation quotient systemtransition system TSabstractBakTSabstractBak= TSBak /∼forAP = { crit1 , crit2 }.Whereas the original transition system is infinite, its bisimulation quotient is finite.Theorem 7.14.Bisimulation Equivalence of TS and TS/ ∼For any transition system TS it holds that TS ∼ TS/ ∼.Proof: Follows immediately from the fact that { (s, s ) | s ∈ [s]∼ , s ∈ S } is a bisimulationfor (TS, TS/R) in the sense of Definition 7.1 (page 451).Bisimulation465In general, the quotient transition system TS/R with respect to a bisimulation R containsmore states than TS/∼ since ∼ is the coarsest bisimulation relation.

It is often simple tomanually indicate a (meaningful) bisimulation, while the computation of the quotientspace S/∼ requires an algorithmic analysis of the complete transition system (see Section7.3 on page 476 and further). Therefore, it may be advantageous to generate the quotientsystem TS/R instead of TS/∼.7.1.2Action-Based BisimulationAs the prime interest of this monograph is model checking, the notions of bisimulationare all focused on the state labelings; labels of transitions are simply ignored.

In othercontexts, most notably process algebras, analogous notions of bisimulation are consideredthat do the reverse—these notions ignore state labelings and are focused on transitionslabels, i.e. actions. The aim of this subsection is to relate these notions.Definition 7.15.Action-Based Bisimulation EquivalenceLet TSi = (Si , Act, →i , Ii , APi , Li ), i=1, 2, be transition systems over the set Act ofactions. An action-based bisimulation for (TS1 , TS2 ) is a binary relation R ⊆ S1 × S2 suchthat(A) ∀s1 ∈ I1 ∃s2 ∈ I2 .

(s1 , s2 ) ∈ R and ∀s2 ∈ I2 ∃s1 ∈ I1 . (s1 , s2 ) ∈ R(B) for any (s1 , s2 ) ∈ R it holds thatαα→ 1 s1 , then s2 −−→ 2 s2 with (s1 , s2 ) ∈ R for some s2 ∈ S2(2’) if s1 −−αα(3’) if s2 −−→ 2 s2 , then s1 −−→ 1 s1 with (s1 , s2 ) ∈ R, for some s1 ∈ S1 .TS1 and TS2 are action-based bisimulation equivalent (or action-based bisimilar), denotedTS1 ∼Act TS2 , if there exists an action-based bisimulation R for (TS1 , TS2 ).Action-based bisimulation differs from the variant for state labels (see Definition 7.1) inthe following way: the state-labeling condition (B.1) is reformulated by means of thetransition labels, and thus is encoded by conditions (B.2’) and (B.3’).