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)
 
Search WWH ::




Custom Search