Information Technology Reference
In-Depth Information
4.2
Workset Based Strategies
In Section 4.1, we suggested the use of partitioning techniques to deal with the large
number of intermediate BDD nodes. However, using partitioning techniques alone is
not enough to yield efficient BDD-based reachability algorithms. In [16], it has been
shown that random structural reachability search yields poor compression of intermedi-
ate BDD nodes. In order to improve these algorithms to substantially reduce the num-
ber of intermediate BDD nodes, it is vital to search the state space in a structural and
efficient way. Here we introduce a simple algorithm, Algorithm 3, which is formally
defined in [13]. The workset algorithm maintains a set of active disjunctive transition
functions
W
k
. These active transition functions are selected one at a time for the local
reachability search. If there is any new state found for the currently selected transition
relation, then all of its
dependent transition functions
(8) will be added in
W
k
. Notice
that in Algorithm 3, ”
” can be any event, since we don't care about the specific events
as long as it is defined in
δ
i
.
·
E
(
δ
i
)=
δ
j
A
j
D
(
A
i
)
A
i
{
|
∈
\{
}}
.
(8)
Algorithm 3 .
Workset forward reachbility algorithm.
δ
1
,...,δ
n
1:
input
:
Q
init
, {
}
δ
1
,...,δ
n
2:
let
W
0
:=
{
},Q
0
:=
Q
init
,k
:= 0;
3:
repeat
4:
H
: Pick and remove a transition
δ
i
∈ W
k
;
k
:=
k
+1;
5:
Q
k
:=
Q
k−
1
∪{q |∃q ∈ Q
k−
1
, δ
i
(
q,·
)=
q}
;
6:
7:
if
Q
k
=
Q
k−
1
then
E
(
δ
i
);
8:
W
k
:=
W
k−
1
∪
9:
end if
10:
until
W
=
∅
11:
return
Q
k
Selection Heuristics.
denotes the heuristics of selecting the next
disjunctive transition function for the reachability search such that the number of in-
termediate BDD nodes is computed as small as possible. How a disjunctive transition
function
δ
i
is chosen among those in the working set has great influence on the perfor-
mance of the algorithm. Here we suggest a series of simple heuristics that have been im-
plemented and seem to work well for real-world problems. In Section 6, those heuristics
will be applied to a benchmark example to compare how they influence the performance
of the workset algorithm.
To find a good heuristic, a two-stage selection rule was implemented, as Fig. 3 shows.
Using this method, a complex selection procedure can be described as a combination
of two selection rules. In the current implementation, the first stage
H
1
selects a subset
W
⊂
In Algorithm 3,
H
W
to be sent to
H
2
using one of the following rules:
