Information Technology Reference
In-Depth Information
4.5 Step 2 with Antichains: From
LSafe
(
ua
)
to
Safe
(
ua
)
The second step for computing
Safe
(
ua
)
from
Safe
(
u
)
relies on the intro-
duction of antichains in Equivalence (4). Implication (
⇒
) holds with antichains:
C
)
.
(8)
Similarly to Implication (6), we can restrict
h
-predecessors to only consider
minimal ones:
∃C
∈
C ∈
Safe
(
ua
)
⇒∀
h
∈
H
Σ
,
LSafe
(
ua
)
,
C ∈
=
Pred
h
(
C
h
-predecessor
of
C
,
C
⊆ C
=
⇒ C
=
C
. Moreover, by Lemma 2, we can limit the
computations to hedges
h ∈ H
where
H
is the finite set introduced in Section 4.1.
Therefore, we obtain the next equality.
C
if for all
C
is a
minimal
h
-predecessor
of
Safe
(
ua
)
=
=
C
∈
C | C
h∈H
C
h
with
C
h
a minimal
h
-predecessor of
LSafe
(
ua
)
(9)
4.6 Algorithm
We are now able to give our antichain-based algorithm (see Algorithm 2). It
uses a stack
(initially empty) as recalled at the beginning of this section. The
computation of
S
H
is considered as a
preprocessing
, as its value only depends
on
A
and not on [
t
0
]. The used results are mentioned inside the algorithm.
5 Improvements and Implementation
Section 4 resulted in a first algorithm for incrementally testing whether a VPA
is right-universal. In this section, we show how this algorithm can be improved
by limiting hedges to consider, and optimizing operators and predecessors to be
computed. We also give the improved algorithm in a more detail way than in
Algorithm 2, as well as the underlying data structures.
5.1 Minimal Hedges
A first improvement is obtained by further restricting hedges to consider. Indeed
it suces to consider
minimal hedges
wrt their function
rel
h
. Formally, let us
write
h
h
whenever
rel
h
(
q
)
≤
⊆
rel
h
(
q
) for every
q
∈
Q
.Wedenoteby
H
the
≤
-minimal elements of
H
. From the definition of
h
-predecessor, we have:
C
C
and
h
h
=
h
-predecessor of
C
h
-predecessor of
≤
⇒ C
(10)
This property can be used to replace
h
∈
H
in (9) by
h
∈
H
:
Safe
(
ua
)
=
⎣
⎧
⎨
⎩
C | C
⎫
⎬
⎦
=
h∈H
C
∈
C
h
with
C
h
a minimal
h
-predecessor of
LSafe
(
ua
)
⎭
(11)
