论文标题
使Streett的确定性紧密
Making Streett Determinization Tight
论文作者
论文摘要
Streett Automata的最佳确定性构建是一个重要的研究问题，因为它在许多应用中是必不可少的，例如树木时间逻辑，逻辑游戏和系统综合的决策问题。本文提出了从非确定性Streett Automata（NSA）带有$ n $状态和$ k $ streett对的转变，再到等效的确定性Rabin Transition Automatiation Automata（drta），带有$ n^{5n}（n！）（n！）^{n} $ state $ n^{5n} k^{nk} $状态，$ o（k^{nk}）$ rabin对$ k = o（n）$。这可以通过$ n^{5n}（n！）^{n+1} $状态，$ o（n^2）$ o（n^2）$ n^{5n} k^{nk} nk} n！$（nk} n！$ o（nk）$ o（nk）$ rabin pairs，这改善了最先进的街道确定化结构。此外，确定性均衡过渡自动机（DPTA）以$ 3（n（n+1）-1）！（n！）^{n+1} $状态，$ 2N（n+1）$优先级，$ k =ω（n）$和$ 3（n）$和$ 3（n（k+1）-1）-1）-1）！ $ k = o（n）$，它以$ n^{n}（k+1）^{n（k+1）}（n（k+1）-1）！$状态，$ 2N（k+1）$优先级来改善最佳结构。此外，我们证明了从NSA到确定性Rabin（过渡）自动机的确定性结构的下限状态复杂性，即$ n^{5n}（n！n！）^{n} $ for $ k =ω（n）$和$ n^{5n^{5n} k^{nk} $ for $ k = o（n）$（n）$，该conscement for Matches for Matches for Matches for Matches for Matches，此外，我们提出了从NSA到确定性均衡（过渡）自动化的下限状态复杂性，即$ 2^{ω（n^2 \ log n）} $ for $ k =ω（n）$和$ 2^{ω（NK \ fog nk \ log nk \ log nk）$ for $ k = o（n）$（n exporents），该exportions的确定是相同的，该exportions的确定是相同的。
Optimal determinization construction of Streett automata is an important research problem because it is indispensable in numerous applications such as decision problems for tree temporal logics, logic games and system synthesis. This paper presents a transformation from nondeterministic Streett automata (NSA) with $n$ states and $k$ Streett pairs to equivalent deterministic Rabin transition automata (DRTA) with $n^{5n}(n!)^{n}$ states, $O(n^{n^2})$ Rabin pairs for $k=ω(n)$ and $n^{5n}k^{nk}$ states, $O(k^{nk})$ Rabin pairs for $k=O(n)$. This improves the state of the art Streett determinization construction with $n^{5n}(n!)^{n+1}$ states, $O(n^2)$ Rabin pairs and $n^{5n}k^{nk}n!$ states, $O(nk)$ Rabin pairs, respectively. Moreover, deterministic parity transition automata (DPTA) are obtained with $3(n(n+1)-1)!(n!)^{n+1}$ states, $2n(n+1)$ priorities for $k=ω(n)$ and $3(n(k+1)-1)!n!k^{nk}$ states, $2n(k+1)$ priorities for $k=O(n)$, which improves the best construction with $n^{n}(k+1)^{n(k+1)}(n(k+1)-1)!$ states, $2n(k+1)$ priorities. Further, we prove a lower bound state complexity for determinization construction from NSA to deterministic Rabin (transition) automata i.e. $n^{5n}(n!)^{n}$ for $k=ω(n)$ and $n^{5n}k^{nk}$ for $k=O(n)$, which matches the state complexity of the proposed determinization construction. Besides, we put forward a lower bound state complexity for determinization construction from NSA to deterministic parity (transition) automata i.e. $2^{Ω(n^2 \log n)}$ for $k=ω(n)$ and $2^{Ω(nk \log nk)}$ for $k=O(n)$, which is the same as the state complexity of the proposed determinization construction in the exponent.
