Information Technology Reference
In-Depth Information
S ` E ; p )
S p ` E (Φ)
S ` E ;: p )
S p ` E (Φ)
R A + :
R A :
S ` E ; f U g )
S ` E ; g )
S ` E ; f ^ g )
S ` E ; f ; g )
R U :
R ^ :
S ` E ; f ; X f U g )
S ` E ; f R g )
S ` E ; f ; g )
S ` E ; f _ g )
S ` E ; f )
R R :
R _ :
S ` E ; g ; X f R g )
S ` E ; g )
S ` E ; F f )
S ` E ; f )
S ` E ; G f )
S ` E ; f ; XG f )
R F :
R G :
S ` E ; XF f )
S
`
E (
Φ
)
S = S 1 [ [ S k ;
R split :
S i 6 = fg;
for i = 1 ::: k
S 1 ` E (Φ)
S k ` E (Φ)
R X : S ` E ( X Φ 1 ;:::; X Φ n )
T ` E 1 ;:::; Φ n )
T =Img( S )
Fig. 2. M-Rules: Multiple state tableau rules (' S p 'and' S p ' are defined in the text).
M-Sequent holds in a Kripke structure K iff S
j
=
Φ 1 ^^ Φ n ,i.e.thereexistsapath
π
in K with
Φ 1 ^^ Φ n . An M-Tableau is a rooted finite directed graph
of nodes labeled with M-Sequents that are connected via the rules shown in figure 2,
where we define the following short hand for p
π
(0)
2
S and
π j
=
A :
2
S p :=
S p :=
f
2
j
2 `
g;
f
2
j
62 `
g
s
S
p
( s )
s
S
p
( s )
In the split rule R split the set of states S on the LHS is partitioned into a nonempty
pairwise disjunctive list of sets S 1 ;:::;
S k that cover S . For M-Tableaux we require every
node to be labeled with a unique M-Sequent. M-Paths, successful M-Path, and SCC are
defined exactly as in the single state case of the last section. The only exception is a
finite M-Path ending with an M-Sequent
), with an empty set of states on
the left side. By definition, such an M-Path is always unsuccessful even if the list of
formulae
fg `
E (
Φ
is empty.
To lift Theorem 1, Theorem 2, and in particular Lemma 3 to M-Tableaux we first
note that the definitions of successful paths, SCCs, and successful tableau do only de-
pend on the RHS of the sequents, in both cases, for S-Tableaux and M-Tableaux. As an
immediate consequence we have:
Φ
Theorem 4. A partially unsuccessful M-Tableau is successful iff it contains a success-
ful SCC.
Lemma 5. An M-Tableau contains an infinite successful M-Path iff it contains a suc-
cessful SCC.
The second step is to map an M-Tableau to a set of S-Tableau, where the M-Tableau is
successful iff one S-Tableau is successful. The mapping
Ψ 0 is defined along the graph
 
Search WWH ::




Custom Search