Information Technology Reference
In-Depth Information
4.2 Antichains
Let us now introduce antichains. Consider the set 2
Q×Γ
∗
of all sets of configura-
tions, with the
operator. An
antichain
is a set of pairwise incomparable sets
of configurations with respect to
⊆
⊆
. Given a set
α
of sets of configurations, we
denote by
α
the
⊆
-minimal
elements of
α
.Theset
α
is
⊆
-upward closed
if for
C ⊆ C
,wehave
C
∈
all
C ∈
α
and
α
. From their definition, it is immediate
that
Safe
(
u
),
LSafe
(
u
),
Pred
a
(
C
)and
Pred
h
(
C
)are
⊆
-upward closed sets.
The idea is to compute the antichain
Safe
(
u
)
(resp.
LSafe
(
u
)
) instead of
the whole
-upward closed set
Safe
(
u
)(resp.
LSafe
(
u
)). The next corollary of
Theorem 1 indicates that such a limited computation is enough to check whether
aVPA
⊆
A
is right-universal w.r.t.
u
.
Corollary 1.
A
is right-universal w.r.t.
u
iff there exists
C∈
Safe
(
u
)
such that
C⊆
Reach
(
u
)
.
Moreover, it can be shown that the antichains
Safe
(
u
)
and
LSafe
(
u
)
are
Γ
k
for
some
k
. We now try to use these antichains at the starting point, and in Steps 1
and 2 of our approach.
finite and only contain finite sets
C
of configurations such that
C ⊆
Q
×
4.3 Starting Point with Antichains
Let us explain how to compute
Safe
(
a
). Clearly, by definition of
H
and using
(1) (see Section 3.2), we can compute
Safe
(
a
)
as follows:
=
(
q
f
,
)
.
(5)
:(
q,σ
)
ha
Safe
(
a
)
C |∀
h
∈
H,
∃
q
f
∈
Q
f
,
∃
(
q,σ
)
∈ C
−→
4.4 Step 1 with Antichains: From
Safe
(
u
)
to
LSafe
(
ua
)
For the two steps, the goal is to adapt Proposition 1 so that it uses
Safe
(
.
)
instead of
Safe
(
.
), and
LSafe
(
.
)
instead of
LSafe
(
.
). We begin with Step 1.
⇒
Implication (
) of Equivalence (3) can be directly adapted.
⇒∃C
∈
C
)
.
C ∈
LSafe
(
ua
)
=
Safe
(
u
)
,
C ∈
Pred
a
(
(6)
Implication (6) gives us a way to compute
LSafe
(
ua
)
from
Safe
(
u
)
:it
suces to take all
a
-predecessors of elements of
Safe
(
u
)
and then limit to
those predecessors that are
⊆
-minimal. We can even only consider minimal
a
-
predecessors of
Safe
(
u
)
in the following sense:
C
is a
minimal
a
-predecessor
of
C
if for all
C
a
-predecessor of
C
,
C
⊆ C
⇒ C
=
=
C
. We finally obtain:
C
∈
LSafe
(
ua
)
=
{C | C
is a minimal
a
-predecessor of
Safe
(
u
)
}
.
(7)