English

Determinization of $\omega$-automata unified

Formal Languages and Automata Theory 2015-03-17 v2 Logic in Computer Science

Abstract

We describe a uniform construction for converting ω\omega-automata with arbitrary acceptance conditions (based on the notion of infinity sets i.e. the set of states visited infinitely often in a run of the automaton) to equivalent deterministic parity automata (DPW). Given a non-deterministic automaton with nn states, our construction gives a DPW with at most 2O(n2logn)2^{O(n^2 \log n)} states and O(n2)O(n^2) parity indices. The corresponding bounds when the original automaton is deterministic are O(n!) and O(n), respectively. Our algorithm gives better asymptotic bounds on the number of states and parity indices vis-a-vis the best known technique when determinizing Rabin or Streett automata with Ω(2n)\Omega{(2^n)} acceptance pairs, where n>1n > 1. We demonstrate this by describing a family of Streett (and Rabin) automata with 2n2^{n} non-redundant acceptance pairs, for which the best known determinization technique gives a DPW with at least Ω(2(n3))\Omega{(2^{(n^3)})} states, while our construction constructs a DRW/DPW with 2O(n2logn)2^{O(n^2\log n)} states. An easy corollary of our construction is that an ω\omega-language with Rabin index kk cannot be recognized by any ω\omega-automaton (deterministic or non-deterministic) with fewer than O(k)O(\sqrt{k}) states.

Keywords

Cite

@article{arxiv.1101.1841,
  title  = {Determinization of $\omega$-automata unified},
  author = {Hrishikesh Karmarkar and Supratik Chakraborty},
  journal= {arXiv preprint arXiv:1101.1841},
  year   = {2015}
}