Research On The Determinization Of Streett Automata

Determinization of a nondeterministic automaton is to construct another deterministic au-tomaton that recognizes the same language as the nondeterministic one,which is one of the fundamental notions in automata theory.Determinization ofωautomata（i.e.finite state automata that can recognize infinite words）is beneficial for complementation,severs as a natural basic step in the decision procedures of SnS,CTL^*,Δ-PDL andμ-calculus etc,and provides theoretical prospects for model checking.Meanwhile,it is also the key of solv-ing infinite games.Therefore,it is of great significance to study the determinization ofωautomata.Seeking the optimal determinization algorithm is also an important problem in computational complexity theory.This dissertation focuses on a kind ofωautomata called Streett automata.Through the tree construction,rather than the subset construction,nondeterministic Streett（transition）automata（NS（T）A）can be determined to equivalent Rabin or parity automata.The upper and lower bounds of state complexity for determinization construction from Streett to Rabin automata are only asymptotically matched.Besides,there is a big gap between the upper and lower bounds of state complexity for determinization construction from Streett to parity automata.In order to make the state complexity for Streett determinization construction tight or tighter.This dissertation focuses on the determinization of Streett automata.The main work is summarized as follows:First of all,we propose a determinization algorithm with optimal state complexity from Streett to Rabin automata.Based on the existing determinization construction calledμ-safra trees,we introduce an index naming scheme,that is,the name of a node depends only on its index label and the position in the tree,which cleverly avoids the influence of names on the state complexity.As a result,a new determinization construction,called H-safra trees,is obtained.Based on H-Safra trees,there is a transformation from NSA with n states and k Streett pairs to equivalent deterministic Rabin transition automata（DRTA）with n⁵ⁿ（n!）ⁿstates for k=ω（n）and n⁵ⁿk^nkstate for k=O（n）.Using the same construction,equiva-lent DRTA with n³ⁿk^n（k+2）states can be constructed from NSTA with n states and k Streett pairs.These improve the state of the art state complexity for determinization construction from Streett to Rabin automata.Further,we define a full Streett transition automaton,which has a rich alphabet and allows all possible transitions,and an L-game recognizing the same language as the full Streett transition automaton.In the L-game,each H-Safra tree of the full Streett transition automaton corresponds to an unique position.Different H-Safra trees correspond to different positions.The moves of the L-game are defined by the structural differences between different H-safra trees.Then,according to the relationship between L-games and deterministic Rabin automata,we prove a lower bound of state complexity for determinization construction from NSTA to DRTA i.e.n³ⁿk^n（k+2）,which matches the state complexity of the proposed determinization construction.It indicates that the determiniza-tion algorithm with H-Safra trees is optimal on state complexity,which completely ends the state complexity of determinization construction from Streett to Rabin automata.Secondly,a determinization algorithm with asymptotically optimal state complexity from Streett to parity automata is proposed.In the determinization procedure,the naming scheme of nodes in the tree needs to be able to describe the generation order of nodes.In order to make full use of the advantages of H-safra trees,a set of all nodes named LIR（Later Intro-duction Record）is added to H-Safra trees.All nodes in the LIR are arranged in the order of generation.Now we get a new determinization construction,called LIR-H-safra trees.By LIR-H-Safra trees,deterministic parity transition automata（DPTA）are obtained with3（n（n+1）-1）!（n!）ⁿ⁺¹states for k=ω（n）and 3（n（k+1）-1）!n!k^nkstates for k=O（n）from NSA.Moverover,from NSTA,DRTA are obtained with 3（n（k+1）-1）!n!k^nkstates.These improve the state of the art state complexity for determinization construction from Streett to parity automata.Similarly,an L-game is also defined that recognizes the complementation of the full Streett transition automaton.We select a subset of all LIR-H-Safra trees of the full Streett transition automaton to correspond to each position in the L-game.Thus,we put forward a lower bound of state complexity for determinization construction from NSTA to DPTA i.e.2^{Ω（nk log nk）},which is the same as the state complexity of the proposed deter-minization construction in the exponent.It indicates that the determinization algorithm with H-Safra trees is asymptotically optimal on state complexity,which greatly reduces the gap between the upper and lower bounds of the state complexity for determinization construction from Streett to parity automata.Finally,a tool named NS2DR&PA is implemented for the determinization of Streett au-tomata.For evaluating the theoretical results of proposed algorithms and showing the pro-cedure of determinization visually,we implement a tool for Streett determinization called NS2DR&PA based on GOAL（Graphical Tool for Omega-Automata and Logics）.The tool supports four determinization constructions,includingμ-Safra trees,H-Safra trees,compact Streett Safra trees and LIR-H-Safra trees.In addition,the tool supports graphical interac-tion,which is convenient to intuitively complete the relevant operations of Streett automata.The resultant deterministic automata can be displayed vividly,and the tree construction cor-responding to each state can also be viewed.Next,a benchmark is constructed by randomly generating 100 Streett automata.We implement these determinization constructions on the benchmark in NS2DR&PA,which shows that experimental results are consistent with theo-retical analyses on state complexity.Moreover,the efficiency of different algorithms is also compared and analyzed.