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

visit of Z (0). Termination is guaranteed because the set of states in Z (0) is finite. Then
z is defined as the path segment from the last occurrence of the same S-Sequent to the
first. From z (0) we can find a finite prefix y to the root as in the finite case.
By construction T S = Ψ( T M ; X (0) ; x (0)) is defined, matches T M , contains the suc-
cessful S-Path x ,and x matches X .

t

1

2

B

A

5

3

4

6

Y

Z

Fig. 3. Extracting an S-Path from an M-Path.

Consider the example of figure 3 where each ellipsis depicts the LHS of a sequent on
which the R X rule is applied. The small filled circles represent single states of the Kripke
structure. The arrows between those circles are transitions of the Kripke structure. Thus
the picture visualizes a sequence Y Z ω of set of states with Y (1)=Img( Y (0)) and

Z (0)=Img( Y (1)) ; Z (1)=Img( Z (0)) ; Z (2)=Img( Z (1)) ; Z (0)=Img( Z (2))

Z ω . We start with 1, transition
to 2 and pick 3 as predecessor of 2. The next transition, from 3 to 4, brings us back to
the last sequent of Z but no cycle can be closed yet. We continue with 5 and reach 3
again with 6. From there we find a prefix (B

Our goal is to extract a sequence of single states from Y

A), that leads from the initial state B to
the start of the cycle at 6. The resulting witness is (B

;

4) ω .
Lemma 6 allows us to derive the following completeness and correctness result for
M-Tableau. Recall that S

; A) (6 ; 5 ;

j = f iff there exists s 2 S with s j = f .

Theorem 7. An M-Tableau with root S ` E ( f ) is successful iff S j = f.

Proof. If an M-Tableau T M is successful then it contains a successful path. Using
Lemma 6 we can construct a matching successful path in a matching S-Tableau T S
with root sequent s ` E ( f ) and s 2 S . The correctness of the S-Tableaux construction

(one part of Theorem 1) proves s = f .

Now let T M be unsuccessful. Then for every s 2 S every matching S-Tableau T S
with root s

j = f whichinturnimplies S j

` E ( f ) is unsuccessful as well. With Theorem 1 we conclude s 6j = f for all

s 2 S . t