环境友好的 GR(1) 综合
计算机科学中的逻辑
2019-02-18 v1
摘要
反应式综合中的许多问题借助两个公式陈述——一个环境假设与一个系统保证——并要求给出一个实现，该实现在满足其假设的环境中满足该保证。反应式综合工具常产生形式上满足此类规约、却通过主动阻止环境假设成立来达成的策略。尽管形式上正确，此类策略并未捕捉设计者的意图。我们在反应式综合中引入一项附加要求，即无冲突性，其要求系统策略应始终允许环境达成其活性要求。我们给出一种求解 GR(1) 综合的算法，其产生无冲突策略。我们的算法由 -演算中的一个 4 层嵌套不动点给出，相对于通常 GR(1) 的 3 层嵌套不动点。我们的算法确保，在每一个自行满足其假设的环境中，所得实现的迹同时满足假设与保证。此外，我们算法的渐近复杂度与通常的 GR(1) 解法相同。我们已实现该算法，并展示其性能与通常 GR(1) 综合算法的比较。
引用
@article{arxiv.1902.05629,
title = {Environmentally-friendly GR(1) Synthesis},
author = {Rupak Majumdar and Nir Piterman and Anne-Kathrin Schmuck},
journal= {arXiv preprint arXiv:1902.05629},
year = {2019}
}
备注
Full version of the TACAS'19 paper with the same title