论自动机最小化在反应式综合中的威力
形式语言与自动机理论
2021-09-20 v2
摘要
时序逻辑常用于描述人工智能应用中的时序性质。最流行的此类语言是线性时序逻辑（LTL）。近来，有限迹上的 LTL（LTLf）已在多个背景下被研究。为了对 LTLf 进行推理，公式通常被编译为确定性有限自动机（DFA）作为中间语义表示。此外，由于 DFA 具有规范表示，可应用高效最小化算法以极大缩减 DFA 规模，从而加速后续计算。在此，我们对两种经典最小化算法，即 Hopcroft 和 Brzozowski 算法，进行了深入研究。更具体地，我们展示了如何将这些算法应用于半符号（显式状态、符号转移函数）自动机表示。随后我们在以 LTLf 公式为起点的 LTLf 综合框架中比较了这两种算法。虽然早先从随机生成自动机出发比较两算法的研究认为不存在某算法占优，我们的结果表明，从 LTLf 公式出发，在反应式综合背景下 Hopcroft 算法是最佳选择。更深入的分析解释了 Brzozowski 算法所谓优势为何在实践中未显现。
引用
@article{arxiv.2008.06790,
title = {On the Power of Automata Minimization in Reactive Synthesis},
author = {Shufang Zhu and Lucas M. Tabajara and Geguang Pu and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:2008.06790},
year = {2021}
}
备注
In Proceedings GandALF 2021, arXiv:2109.07798