From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata

TL;DR

This paper improves the determinization process for automata on infinite words by creating smaller deterministic automata with parity acceptance, enhancing efficiency in various formal verification applications.

Contribution

It introduces a new construction that reduces the size of deterministic automata and simplifies acceptance conditions from Rabin or Streett to parity.

Findings

Fewer states in deterministic automata.

Parity acceptance conditions enable more efficient algorithms.

Reduced upper bounds in applications like model checking and synthesis.

Abstract

In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).