Information Technology Reference
In-Depth Information
The algorithm described in the proof of Lemma 6 can be used to construct a witness
for the root sequent from a successful M-Tableau, or a counterexample for the negation
of the root sequent. First a matching path is constructed. Then a witness, a finite or
cyclic path of states, can easily be extracted.
5
Algorithm
A more detailed description of the tableau construction follows in this section. The
overall approach expands open branches in DFS manner and stops when a successful
finite path has been generated, a successful SCC has been found, or finally no rule can
be applied without regenerating an edge that already exists in the tableau. In the first
two cases a witness for the root sequent can be generated. In the last case it is shown
that the root sequent can not hold.
Finite successful paths are easy to detect. To detect and not to miss any successful
SCC we use a modified version of Tarjan's algorithm for decomposing a directed graph
into its strongly connected components. It is the same algorithm as used for S-Tableau
in Section 3.
During the construction we have to remember the sequents that already occurred
in the tableau. This can be accomplished by a partial function mapping a sequent to a
node. To implement this we can sort the sequents in the tableau, use a hash table, or
simply an array. In practice a hash table is the best solution.
Up to this point the algorithm is identical for both, single and multiple state tableaux.
Our intention, of course, is to represent set of states with BDDs. We associate with each
formula
E
(
Φ
) the list of sequents in the tableau that have
E
(
Φ
) on the RHS. To check
if a sequent
σ
(
S
`
E
(
Φ
) already occurred, we just go through the list of sequents
associated with
E
(
) and check whether the BDD representing the set of states on the
LHS of one of the sequents in the list is the same as the BDD representing
S
.
Φ
6
Heuristics
The rule
R
split
is not really necessary for the completeness but it helps to reduce the
search space, i.e. the size of the generated tableau. For instance consider the construc-
tion of a tableau for the formula
EF
p
. This formula is the negation of a simple safety
property. In this case a good heuristics is to build the tableau by expanding the left suc-
cessoroftherule
R
F
first. Only if the left branch does not yield a successful path, then
the right successor is tried. If during this process a sequent
σ
0
=
S
0
`
E
(
F
f
) is found
σ
00
=
S
00
`
σ
0
and
S
00
S
0
then
and a sequent
E
(
F
f
) occurs on the path from the root to
we can remove the set
S
00
from
S
0
by applying
R
split
with
S
1
=
S
00
and
S
2
=
S
0
−
S
00
.The
left successor immediately leads to an unsuccessful infinite path and we can continue
with the right successor.
A successful path in a tableau for
EF
p
is a counterexample for the dual safety prop-
erty
AG
p
. Thus applying the heuristic of the last paragraph essentially implements
an algorithm that computes the set of reachable states in a BFS manner while checking
on-the-fly for states violating the safety property (as the
early evaluation
technique in
:
Search WWH ::
Custom Search