Abstract:Determinization of a nondeterministic automaton is to construct another deterministic automaton that recognizes the same language as the nondeterministic one, which is one of the fundamental notions in automata theory. Determinization of ω automata serves as a natural basic step in the decision procedures of SnS, CTL*, μ-calculus etc. Meanwhile, it is also the key of solving infinite games. Therefore, it is of great significance to study the determinization of ω automata. We focus on a kind of ω automata called Streett automata. Nondeterministic Streett automata can be transformed into equivalent deterministic Rabin or parity automata. In our previous work, we have obtained the optimal and asymptotically optimal determinziation algorithms respectively. For evaluating the theoretical results of proposed algorithms and showing the procedure of determinization visually, it is necessary to develop a tool to support Streett determinization. In this paper, we first introduce four different Streett determinization constructions, including μ-Safra trees, H-Safra trees, compact Streett Safra trees and LIR-H-Safra trees. By H-Safra trees, which are optimal, and μ-Safra trees, deterministic Rabin transition automata are obtained. In addition, deterministic parity transition automata are constructed via another two structures, where LIR-H-Safra trees are asymptotically optimal. Further, based on the open source software, named Graphical Tool for Omega-Automata and Logics (GOAL), we implement a tool for Streett determinization, named NS2DR & PT. Besides, a benchmark is constructed by randomly generating 100 Streett automata. We have implemented these determinization constructions on the benchmark in NS2DR & PT, which shows that experimental results are consistent with theoretical analyses on state complexity. Moreover, the efficiency of different algorithms is also compared and analyzed.