This paper deals with the problem of automatically and correctly controlling infinite-state reactive programs to achieve LTL goals. Applications include adapting a program to new requirements, or to repair bugs discovered in the original specification or program code. Existing approaches are able to solve this problem for safety and some reachability properties, but require an a priori template of the solution for more general properties. Fully automated approaches for full LTL exist, reducing the problem into successive finite LTL reactive synthesis problems in an abstraction-refinement loop. However, they do not terminate when the number of steps to be completed depends on unbounded variables. Our main insight is that safety abstractions of the program are not enough -- fairness properties are also essential to be able to decide many interesting problems, something missed by existing automated approaches. We thus go beyond the state-of-the-art to allow for automated reactive program control for full LTL, with automated discovery of the knowledge, including fairness, of the program needed to determine realisability. We further implement the approach in a tool, with an associated DSL for reactive programs, and illustrate the approach through several case studies.

翻译：本文研究如何自动且正确地控制无限状态响应式程序以实现LTL目标。其应用包括使程序适配新需求，或修复原始规范及程序代码中发现的缺陷。现有方法能够解决安全性和部分可达性属性问题，但对于更一般的属性需要预设解决方案模板。针对完整LTL的完全自动化方法虽已存在，通过抽象精化循环将问题逐步简化为有限LTL响应式综合问题，但当所需完成步骤依赖于无界变量时，这些方法无法终止。我们的核心洞察在于：程序的安全性抽象并不足够——公平性属性对于判定大量有趣问题同样至关重要，而现有自动化方法恰恰忽略了这一点。因此，我们突破了现有技术水平，实现了面向完整LTL的自动化响应式程序控制，并能够自动发现程序所需的知识（包括公平性）以确定可实现性。我们进一步将该方法实现为工具，并配套了用于响应式程序的领域特定语言，通过多个案例研究验证了该方法的有效性。