Sleep sets

Abstract

The second technique for computing the set of transitions T to consider in a selec-tive search is the sleep set technique [GW93] introduced in [God90}. This technique does not exploit information about the static structure (code) of tile program, as persistent-set algorithms do, but rather information about the past of the search. Used in conjunction with a persistent-set technique, sleep sets can further reduce the number of states explored. Indeed, when the persistent-set technique cannot avoid the selection of independent transitions in a state, sleep sets can avoid the wasteful exploration of multiple interleavings of these transitions. Example 5.1 Consider a system containing two processes A = {a0, al, a2} and B = {b0, bl, b2}, two objects x and y of type "boolean variable", and four transitions t 1 = (a0, tf%e, x :~-~-0, al) , t 3 = (b0, true, y := 1, bl) , t2 = (al, true, y := 0, a2), t4 = (bl, true, x := 1, b2). Consider the state s = (a0, b0, 0, 0) G A • B x Vx • Vy. In state s, both transitions tl and t3 are enabled. The global state space Ao corresponding to this system is shown