Two-player games are a fruitful way to represent and reason about several important synthesis tasks. These tasks include controller synthesis (where one asks for a controller for a given plant such that the controlled plant satisfies a given temporal specification), program repair (setting values of variables to avoid exceptions), and synchronization synthesis (adding lock/unlock statements in multi-threaded programs to satisfy safety assertions). In all these applications, a solution directly corresponds to a winning strategy for one of the players in the induced game. In turn, \emph{logically-specified} games offer a powerful way to model these tasks for large or infinite-state systems. Much of the techniques proposed for solving such games typically rely on abstraction-refinement or template-based solutions. In this paper, we show how to apply classical fixpoint algorithms, that have hitherto been used in explicit, finite-state, settings, to a symbolic logical setting. We implement our techniques in a tool called GenSys-LTL and show that they are not only effective in synthesizing valid controllers for a variety of challenging benchmarks from the literature, but often compute maximal winning regions and maximally-permissive controllers. We achieve \textbf{46.38X speed-up} over the state of the art and also scale well for non-trivial LTL specifications.

翻译：双人博弈是一种富有成效的方式，可用于表示和推理多种重要的综合任务。这些任务包括控制器综合（即针对给定被控对象，要求设计控制器使得受控对象满足给定的时序规范）、程序修复（通过设置变量值来避免异常）以及同步综合（在多线程程序中添加加锁/解锁语句以满足安全断言）。在所有这些应用中，解决方案直接对应于所诱导博弈中某一玩家的获胜策略。进而，*逻辑指定*博弈为建模这些涉及大规模或无限状态系统的任务提供了强大手段。目前，解决此类博弈的多数技术通常依赖于抽象精化或基于模板的方法。在本文中，我们展示了如何将此前仅用于显式、有限状态场景的经典不动点算法应用于符号逻辑设置。我们将所提出的技术实现于一个名为GenSys-LTL的工具中，并证明这些技术不仅能有效综合出文献中多种具有挑战性基准测试的有效控制器，而且常常能计算出最大获胜区域和最大允许控制器。与现有技术相比，我们实现了**46.38倍的加速**，并且在处理非平凡的LTL规范时也能保持良好的可扩展性。