关于 μ-演算中析取公式的大小
计算机科学中的逻辑
2021-09-20 v1
摘要
模态 μ-演算理论中的一个关键结果是 Janin 与 Walukiewicz 的析取范式定理，该定理指出每个 μ-演算公式在语义上等价于所谓的析取公式。这些析取公式具有良好的计算性质，并在模态 μ-演算理论中起着关键作用。因此，将公式重写为规模最小的等价析取公式的最佳规范化过程是什么，是一个有趣的问题。文献中已知的最佳构造本质上基于自动机，由一个守护变换（即，从 μ-演算公式构造等价的守护交替自动机）以及一个仿真定理（指出任何此类交替自动机可转换为等价的非确定自动机）组成。这两种变换均为指数级构造，使得最佳规范化过程为双指数级。我们在此提出的核心贡献表明，规范化过程的两个部分可以整合，从而得到关于公式闭包大小为单指数的过程。
引用
@article{arxiv.2109.08310,
title = {On the size of disjunctive formulas in the $\mu$-calculus},
author = {Clemens Kupke and Johannes Marti and Yde Venema},
journal= {arXiv preprint arXiv:2109.08310},
year = {2021}
}
备注
In Proceedings GandALF 2021, arXiv:2109.07798