Information Technology Reference
In-Depth Information
the same applies to an S-path. A finite S-Path x is successful iff it ends with a sequent
s
E (), where the list of formulae is empty. An S-Tableau is partially successful iff
the tableau contains a finite successful S-Path. It is partially unsuccessful iff no finite
S-Path is successful.
An eventuality f , contained in the list of formulae of x ( i ), is called fulfilled iff there
exists j with i
`
< j
j
and the body of f is contained in x ( j ). This definition also
applies to infinite paths. An infinite S-Path x is called successful iff every eventuality in
x is fulfilled. Finally a tableau is successful iff it is partially successful or it contains an
infinite successful S-Path. With these definitions we can derive the following theorem
from [2, 19]:
j
x
`
j
Theorem 1. An S-Tableau with root s
E ( f ) is successful iff s
= f.
E ( f ) is successful.
Therefore completeness and correctness is independent of the order in which the rules
are applied. In the construction of the tableau no backtracking is required. The freedom
to choose a rule, if several are applicable, can be used to minimize the size of the
tableau, and thus the running time of the model checking algorithm (see Section 6 and
Section 7).
Finding successful paths seems to be an algorithmically complex problem. How-
ever, we will show that this problem can be reduced to the search for a successful
strongly connected component. A strongly connected component (SCC) of a directed
graph is a maximal subgraph in which every node can be reached from every other node
in the subgraph. Note that in our notation a single node, not contained in any cycle, is
not an SCC. We call an SCC of an S-Tableau successful iff every eventuality occurring
in the SCC is fulfilled in the SCC, i.e. with every eventuality the SCC also contains
its body. For an efficient implementation the following theorem is very important. As
a result the search for a successful infinite path can be replaced by the search for a
successful SCC, which is algorithmically much simpler.
This theorem implies that s
j
= f iff every S-Tableau with root s
`
Theorem 2. A partially unsuccessful S-Tableau is successful iff it contains a successful
SCC.
This theorem is an easy consequence of the following Lemma, which can be used for
the generation of an infinite witness, respectively counterexample, as explained below.
Lemma 3. An S-Tableau contains an infinite successful S-Path iff it contains a success-
ful SCC.
Proof. For the proof from left to right let x be an infinite successful S-Path. First note
that there has to be an SCC C in which a suffix of x is fully contained, since the S-
Tableau is finite. Further let
be a sequent in C with an eventuality f on the right
hand side (RHS). We need to show that f is fulfilled in C .Since C is an SCC, there
exists a path segment connecting
σ
to the start of the suffix of x in C . If the body of f
occurs on this path segment then we are done. Otherwise, by the structure of the rules
for eventualities, the first sequent of the suffix of x in C reached by this segment still
contains f or X f .Since x is successful the body of f has to occur in the suffix of x
which is part of C .
σ
 
Search WWH ::




Custom Search