交替弱 Büchi 自动机到无歧义 Büchi 自动机的单指数翻译

我们引入一种将交替弱 Büchi 自动机（AWA）——对应于线性动态逻辑（LDL）公式——翻译为无歧义 Büchi 自动机（UBA）的方法。我们的翻译推广了针对线性时序逻辑（LTL）的构造，LTL 是比 LDL 表达能力更弱的规定语言。在经典构造中，LTL 公式首先被翻译为交替\emph{极弱}自动机（AVA）——仅含单点强连通分量（SCC）的自动机；随后 AVA 由高效的去歧义过程处理。然而，一般 AWA 可具有更大的 SCC，这使去歧义复杂化。目前唯一的去歧义过程须经过非确定性 Büchi 自动机（NBA）的中间构造，其自身将带来指数级膨胀。我们引入从\emph{一般} AWA 到 UBA 的具有\emph{单}指数膨胀的翻译，这也立即给出了从 LDL 到 UBA 的单指数翻译。有趣的是，我们翻译的复杂度\emph{小于}已知最佳的 NBA 去歧义算法（约为 $(0.53n)^n$ 对比 $(0.76n)^n$），而我们的构造输入可指数级更简洁。