交替弱布基自动机到非二义性布基自动机的单指数翻译
摘要：将对应于线性动态逻辑（LDL）公式的交替弱B"uchi自动机（AWA）翻译为无歧义的B"uchi自动机（UBA）的方法被我们提出。我们的翻译对线性时态逻辑（LTL）进行了推广，LTL是比LDL更少表达性的规范语言。在经典构造中，LTL公式首先被翻译为具有仅包含单例强连通分量（SCC）的交替的非常弱自动机（AVAs） -- 这些自动机然后通过高效的消除二义性的过程进行处理。然而，一般的AWAs可能具有较大的SCCs，这会给消除二义性带来复杂性。目前唯一可用的消除二义性过程必须经过中间的非确定性B"uchi自动机（NBAs）的构建，这将引起其指数级的膨胀。我们引入了一种将一般的AWAs翻译为UBAs的翻译，其产生的膨胀为指数级，这也立即提供了从LDL到UBAs的单指数翻译。有趣的是，我们的翻译的复杂性比现有最佳的NBAs消除二义性算法（广义上为$(0.53n)^n$ vs. $(0.76n)^n$）要小，而我们构造的输入却可以更加精简。
作者：Yong Li, Sven Schewe and Moshe Y. Vardi
论文ID：2305.09966
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-05-18