Database Reference
In-Depth Information
accepting states are those with
as the last component. In order to obtain an UFTA(DFA)
for
[
μ
1
,
μ
2
,...,
μ
n
] it suffices to take the product of
A
[μ
i
]
.
It is not difficult to see that the construction is asymptotically optimal (
Exercise 22.3
).
We can now combine the two ideas and reduce consistency of mappings to the emptiness
problem. Testing emptiness can be done in polynomial time, but the UNFTA resulting from
the reduction will be a product of linearly many UNFTA of exponential size, and hence will
be exponential.
Proposition 18.3 C
ONS
◦
(
⇓
,
⇒
)
is
E
XPTIME
-complete.
Proof
For a mapping (
st
) to be consistent, there must exist a pair (
T
1
,
T
2
) such
that for all ϕ
−→
ψ
∈
Σ
st
it holds that
T
1
|
= ϕ
S
s
,
S
t
,
Σ
implies
T
2
|
= ψ . Suppose Σ
st
=
{
ϕ
i
−→
ψ
i
i
= 1
,
2
,...,
n
}
. Then the existence of such a pair is equivalent to the existence of a subset
I
⊆{
1
,
2
,...,
n
}
satisfying
•
there exists
T
1
|
=
S
s
such that
T
1
|
=
ϕ
j
for all
j
∈
I
,
•
there exists
T
2
|
=
S
t
such that
T
2
|
=
ψ
i
for all
i
∈
I
.
This amounts to nonemptiness of the following automaton:
¯
• A
s
×
∏
j
∈
I
A
ϕ
j
,
• A
t
×
∏
j
∈
I
A
ψ
j
,
where
A
s
and
A
t
are the UNFTA underlying
S
s
and
S
t
. The construction of each
A
ϕ
A
ϕ
takes exponential time. Since
are deterministic, complementing them is straightfor-
A
1
×···×A
k
can be done in time
O
|A
1
|×···×|A
k
|
ward. Testing nonemptiness of
(
).
Hence, the overall complexity is E
XPTIME
.
To prove E
XPTIME
-hardness we provide a reduction from the nonuniversality problem
for binary tree automata (NTAs). Given an NTA
A
, testing if there is a tree rejected by
A
is known to be E
XPTIME
-hard. The idea of the encoding is that the source tree codes
both an input tree and the run of the corresponding deterministic powerset automaton. The
st-tgds ensure that the run is constructed properly, and that it contains only nonfinal states
in the root.
Fix an NTA
A
=(
Q
,
Γ
,
q
0
,
F
,
δ
) with
Q
=
{
q
0
,...,
q
n
}
and
Γ
=
{
a
1
,...,
a
k
}
.Let
S
s
be
given by the DTD
r
,
left
,
right
→
label
q
0
...
q
n
(
leftright
|
leaf
)
label
→
a
1
|
a
2
|
...
|
a
k
q
1
,
q
2
,...,
q
n
→
yes
|
no
and
.
In every tree conforming to
S
by
r
→
ε
S
s
, the nodes labeled with
r
,
left
and
right
form a binary
tree over which we run the powerset automaton. A
q
i
-child should lead to a
yes
iff the state
