论文标题
来自扩展有界响应LTL规范的反应性合成
Reactive Synthesis from Extended Bounded Response LTL Specifications
论文作者
论文摘要
反应性合成是设计正确构造系统的关键技术，并且在过去几十年中已经对其进行了彻底的研究。它由一个控制器的合成，该控制器对满足给定时间逻辑规范的环境输入做出反应。共同的方法基于自动机的明确构造及其确定性，这限制了它们的可扩展性。 在本文中，我们介绍了一个新的线性时间逻辑片段，称为扩展有界响应LTL（\ ltlebr），它允许一个人组合一个有界和通用的无限时间操作员（因此涵盖了大量实际情况），我们显示从\ ltlebr的规格中构建了一个自动化的构建的自动化构建的构建的反应性合成，可以自动构建确定性构建。我们证明了所提出的方法的正确性，并在各种基准上成功评估了它。
Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability. In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (\LTLEBR), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from \LTLEBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.
