LTLf到自动机翻译中的一阶与二阶编码比较
计算机科学中的逻辑
2019-01-21 v1 形式语言与自动机理论
摘要
将有限迹上的线性时序逻辑（LTL）即LTLf的公式翻译为符号化确定性有限自动机（DFA），不仅在LTLf综合中，也在安全LTL公式的综合中起着重要作用。该翻译通过使用MONA实现，MONA是一个强大的用于从逻辑规范构建基于BDD的符号化DFA的工具。近期工作使用LTLf公式的一阶编码将LTLf翻译为一阶逻辑（FOL），随后输入MONA得到符号化DFA。该编码被证明表现良好，但其他编码尚未被研究。具体而言，二阶编码（其量化结构显著更简单）是否能优于一阶编码这一自然问题仍然悬而未决。本文中我们应对这一挑战并研究LTLf公式的二阶编码。我们首先引入一种特定的MSO编码，以自然方式刻画LTLf的语义并证明其正确性。接着我们探索了一种紧凑MSO（Compact MSO）编码，其受益于自动机理论最小化，从而暗示了可能的实际优势。为此，我们在二阶逻辑中提出了符号化DFA的形式化，从而建立了BDD与MSO之间的新联系。随后我们通过实证评估表明，一阶编码确实优于两种二阶编码。结论是，在LTLf到自动机翻译中，一阶编码是比二阶编码更好的选择。
引用
@article{arxiv.1901.06108,
title = {First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation},
author = {Shufang Zhu and Geguang Pu and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1901.06108},
year = {2019}
}