基于可满足性的从安全规约进行反应式合成的方法
计算机科学中的逻辑
2016-04-22 v1
摘要
现有从声明式规约合成反应式系统的方法主要依赖二元决策图（BDDs），继承了它们的可扩展性问题。我们提出了用于安全规约的新算法，这些算法使用命题公式的决策过程（SAT 求解器）、量化布尔公式（QBF 求解器）或有效命题逻辑（EPR）。我们的算法基于查询学习、模板、归约到 EPR、QBF 认证以及插值。一种并行化方法结合了多种算法。我们的优化扩展了量词并利用不可达状态与变量独立性。我们的方法优于简单的基于 BDD 的工具，并与高度优化的工具具有竞争力。它在 SyntComp 竞赛中赢得了两枚奖牌。
引用
@article{arxiv.1604.06204,
title = {Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications},
author = {Roderick Bloem and Uwe Egly and Patrick Klampfl and Robert Könighofer and Florian Lonsing and Martina Seidl},
journal= {arXiv preprint arXiv:1604.06204},
year = {2016}
}
备注
This is the manuscript of an article that has been submitted to the Journal of Computer and System Sciences (JCSS)