Multiple State and Single State Tableaux for Combining Local and Global Model Checking - Correct System Design: Recent Insights and Advances - page 169

partition S = S 1 [ S 2 into two mutually exclusive sets, S 1 and S 2 .If S 2 = fg ,i.e. S 1 is

the only maximal set in P , then we define

P 0 := P S 0 :=

nf g

S 1 and T

T 2 P 0

S 0 j < j and with 0 < j S 1 jj S j the induction hypothesis shows

P 0 j < S 0 j< S 0 j j P j = 1+ j 1+2 j 2 ( j +1) 2 j S 1 j 2 j S j

Now we assume S 2 = fg , which implies S 1 = S , and induces a partition on P with

P = P 1 [ P 2 and P i := f T 2 P j T S i g for i = 1 ; 2

Finally the induction hypothesis applied to S 1 and S 2 results in

j jj j j j< j j j j j j j j j j

P P 1 + P 2 2 S 1 +2 S 2 =2 ( S 1 + S 2 )=2 S

t

Since the LHS of a sequent can also be an empty set, Lemma 8 shows that the
number of sequents with the same RHS is bounded by 2 if the invariant is main-

tained. This is also the best bound that we can get, as the following example shows.
Let S i =

j S j

2 i f 0 ;:::; − 1 g . Then we associate a balanced binary tree of height i with

each P i IP ( S i ) . We label each node in the tree by exactly one element of P i ,which

= 2 i +1

j j − j j−

implies P i 1 = 2 S i 1. The i leaves are labeled with the singleton sets

2 i

f g;:::;f − g

. Each inner node of the binary tree is labeled with the union of the
labels of its children.
Note that the image rule R X and the atomic rules R A + and R A − are the only rules,
except the split rule R split , that actually manipulate the LHS. All other rules only gener-
ate sequents that contain the same set of states as their parents. The application of these
rules can not violate the invariant. To maintain the invariant in the case of R X , R A +
and R A − as well we have to apply the split rule in combination with these rules: After
each image calculation or application of an atomic rule the sequent is split to fulfill the
invariant. For instance if the application of R X yields:

0 1

R X :

f 1 ; 2 ; 3 ; 4 g` E ( Φ )

and the tableau already contains the two sequents:

f 1 ; 2 g` E ( Φ ) and f 4 ; 5 g` E ( Φ )

Then the split rule is applied as follows. For every non empty intersection of f 1 ; 2 ; 3 ; 4 g

with the LHS of an already existing sequent a new sequent is generated:

f 1 ; 2 ; 3 ; 4 g` E ( Φ )

R split :

f 1 ; 2 g` E ( Φ ) f 3 g` E ( Φ ) f 4 g` E ( Φ )