从非确定性 B"uchi 和 Streett 自动机到确定性 Parity 自动机
计算机科学中的逻辑
2019-03-14 v2 形式语言与自动机理论
摘要
本文重新审视了 Safra 关于无限词自动机的确定性构造。我们展示了如何构建状态数更少的确定性自动机,最重要的是,具有 Parity 接受条件。确定性化被用于众多应用,例如树自动机的推理、CTL* 的可满足性,以及逻辑规范的可实现性与合成。通过使用我们构造产生的更小的确定性自动机,所有这些应用的上界都得到了降低。此外,Parity 接受条件允许使用更高效的算法(与处理 Rabin 或 Streett 接受条件相比)。
引用
@article{arxiv.0705.2205,
title = {From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata},
author = {Nir Piterman},
journal= {arXiv preprint arXiv:0705.2205},
year = {2019}
}
备注
21 pages. To appear in Logical Methods in Computer Science (LMCS)