艾默生-雷氏自动机的确定化和极限确定化
摘要：确定性化基于布尔公式定义状态转换的$\omega$-自动机（也被称为基于转换的Emerson-Lei自动机（TELA））的问题。标准的确定化TELA方法首先构造等价的广义布奇自动机（GBA），然后再对其进行确定化。我们引入了三种将TELA转换为GBA的新方法。此外，我们给出了一种新的确定化构造方法，该方法独立地确定化多个GBA，并使用乘积构造方法进行组合。实验评估表明，与现有的确定化过程相比，乘积方法具有竞争力。我们还研究了TELA的极限确定化，并表明这可以通过单指数增长来完成，与已知的确定化的双指数下界形成对比。最后，极限确定化过程的一个版本可以产生适用于定量概率模型检验的好-for-MDP自动机。
作者：Tobias John, Simon Jantsch, Christel Baier and Sascha Kl"uppelholz
论文ID：2106.15892
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-07-01