有界综合的编码
计算机科学中的逻辑
2018-03-28 v1
摘要
反应式综合问题旨在计算一个满足给定时序逻辑规范的系统。有界综合是一种限制我们接受作为反应式综合问题解的系统最大规模的方法。因此，只要相应的验证问题是可判定的，有界综合就是可判定的，并且可以应用于经典综合失效的场景，例如分布式系统的综合。在本文中，我们研究了有界综合背后的约束求解问题。我们考虑了将线性时序逻辑（LTL）的有界综合问题归约为由布尔公式（SAT）、量化布尔公式（QBF）和依赖量化布尔公式（DQBF）给出的约束系统的不同归约方法。这些归约代表了简洁性与算法效率之间的不同权衡。在 SAT 编码中，系统的输入和状态均被显式表示；在 QBF 中，输入是符号化的而状态是显式的；在 DQBF 中，输入和状态均为符号化。我们使用来自反应式综合竞赛（SYNTCOMP）的基准测试和 SOTA 求解器系统地评估了这些编码。我们关键的、或许令人惊讶的经验发现是，QBF 明显优于 SAT 和 DQBF。
引用
@article{arxiv.1803.09570,
title = {Encodings of Bounded Synthesis},
author = {Peter Faymonville and Bernd Finkbeiner and Markus N. Rabe and Leander Tentrup},
journal= {arXiv preprint arXiv:1803.09570},
year = {2018}
}
备注
Appeared in the proceedings of TACAS 2017