Sunday, Nov 27, 2005, 11:15-12:15
Room 309
--------------------------------------------------------------------------------
Nir Piterman
Ecole Polytechnique Fédérale
de Lausanne
Title:
Revisiting Safra's Determinisation of Automata on Infinite Words
Abstract:
Determinization and
complementation are fundamental notions in
computer science.
When considering finite automata on finite words determinization
gives also a solution to
complementation.
Given a nondeterministic finite automaton there exists an
exponential construction that gives
a deterministic automaton for the
same language.
Dualizing the set of accepting
states gives an automaton for
the complement language.
In the theory of automata on infinite words, determinization and
complementation are much more
involved.
Safra provides determinization
constructions for B\"uchi and
Streett automata that result in deterministic Rabin automata.
For a B\"uchi automaton with $n$
states, Safra constructs a
deterministic Rabin automaton with $n^{O(n)}$
states and $n$ pairs.
For a Streett automaton with $n$ states
and $k$ pairs, Safra
constructs a deterministic Rabin
automaton with $(nk)^{O(nk)}$
states
and $n(k+1)$ pairs.
Here, we reconsider Safra's determinization constructions.
We show how to construct automata with fewer states
and, most importantly, parity
acceptance condition.
Specifically, starting from a nondeterministic B\"uchi automaton with
$n$ states our construction yields a deterministic parity
automaton
with $n^{2n+2}$ states and index $2n$
(instead of a Rabin automaton
with $\safrastates$
states and $n$ pairs).
Starting from a nondeterministic Streett
automaton with $n$ states and
$k$ pairs our construction yields a deterministic parity
automaton
with $n^{n(k+2)+2}(k{+}1)^{2n(k+1)}$ states and index $2n(k+1)$
(instead
of a Rabin automaton with $(12)^{n(k+1)}n^{n(k+2)}(k{+}1)^{2n(k+1)}$
states and $n(k+1)$ pairs).
The parity condition is much simpler than the Rabin
condition.
In applications such as solving games and emptiness of tree
automata
handling the Rabin condition
involves an additional multiplier of
$n^2n!$ (or $(n(k+1))^2(n(k+1))!$ in
the case of Streett) which is saved
using our construction.