Information Technology Reference
In-Depth Information
Algorithm 2
Checking right-universality incrementally with antichains
function
Antichain-Based Incremental-Right-universality(
A
,
H
)
Push(
S,Init
)% y ,
S
beingastack
u ←
first letter of [
t
0
]
R ←
Compute
Reach
(
u
)
α ←
Compute
Safe
(
u
)
%by(5)
if
∃C ∈ α
:
C ⊆ R
then
return
True
% Corollary 1
end if
while
[
t
0
] is not completely read
do
a ←
next letter of [
t
0
]
u ← ua
R ←
Compute
Reach
(
u
)from
R
if
a ∈ Σ
then
α ←
Pop(
S
)
else
Push(
S,α
)
α ←
Compute
Safe
(
u
)
from
α
% by (7) and (9)
end if
if
∃C ∈ α
:
C ⊆ R
then
return
True
% by Corollary 1
end if
end while
return
False
end function
and similarly for the starting point:
=
(
q
f
,
)
(12)
:(
q,σ
)
ha
Safe
(
a
)
C |∀
h
∈
H
,
∃
q
f
∈
Q
f
,
∃
(
q,σ
)
∈ C
−→
5.2 An Appropriate Operator
C
Safe
(
ua
)
Equation (11) expresses that every set of configurations
in
is the
C
h
with
h
∈
H
union of
. We introduce a new operator to improve the reada-
bility and find new properties. Let
S
be a finite set, and
A,B
2
2
S
\{∅}
.Theset
∈
2
2
S
is defined by
A
B
∈
A
B
=
{
a
∪
b
|
a
∈
A
and
b
∈
B
}
.
Operator
builds sets obtained by taking one set of each of its operands, and
performing their union. It is obviously associative and commutative. Notice that
the elements of
A,B
are supposed to be non empty sets. This is always the case
in the algorithms using this operator.
When combined with operator
.
, operands of the
operator can be splitted,
so that
is to be computed on smaller sets:
A
B
=
(
A
∩
B
)
∪
(
A
\
B
B
\
A
)
(13)
