一句话：改进了 Streett 自动机确定化的状态复杂度，并证明匹配下界，使其达到紧界。
本文研究非确定性 Streett 自动机（NSA）的确定化问题，该问题在树时序逻辑判定、逻辑博弈与系统综合中至关重要。作者提出新的确定化变换，将具有 n 个状态和 k 个 Streett 对的 NSA 转为等价的确定性 Rabin 转移自动机（DRTA）与确定性奇偶转移自动机（DPTA）。在 k=ω(n) 与 k=O(n) 两种情形下，DRTA 状态数分别改进为 n5^n(n!)^n 和 n5^n k^n n^k，DPTA 也取得更优状态数与 2n(n+1) 或 2n(k+1) 个优先级。作者还证明 NSA 到确定性 Rabin（转移）自动机的状态复杂度下界与所提构造匹配，并给出到确定性奇偶（转移）自动机的指数级下界，从而使 Streett 确定化达到紧界。
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 n5n(n!)n states, O(nn2) Rabin pairs for k = ω(n) and n5nknk states, O(knk) Rabin pairs for k = O(n). This improves the state of the art Streett determinization construction with n5n(n!)n+1 states, O(n2) Rabin pairs and n5nknkn! 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!knk states, 2n(k + 1) priorities for k = O(n), which improves the best construction with nn(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 N-SA to deterministic Rabin (transition) automata i.e. n5n(n!)n for k = ω(n) and n5nknk 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ω(n2 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.
DOI 原文 ·
@inproceedings{paperbot5500,
title = {Making Streett Determinization Tight},
author = {Cong Tian and Wensheng Wang and Zhenhua Duan},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394757}
}