The synthesis of reactive systems aims for the automated construction of strategies for systems that interact with their environment. Whereas the synthesis approach has the potential to change the development of reactive systems significantly due to the avoidance of manual implementation, it still suffers from a lack of efficient synthesis algorithms for many application scenarios. The translation of the system specification into an automaton that allows for strategy construction is nonelementary in the length of the specification in S1S and double exponential for LTL, raising the need of highly specialized algorithms. In this paper, we present an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotony property of specifications. For this, we introduce window counting constraints that allow for step-wise refinement or abstraction of specifications. In an iterating synthesis procedure, those window counting constraints are used to construct automata representing over- or under-approximations (depending on the counting constraint) of constraint-compliant behavior. Analysis results on winning regions of previous iterations are used to reduce the size of the next automaton, leading to an overall reduction of the state space explosion extend. We present the implementation results of the iterated synthesis for a zero-sum game setting as proof of concept. Furthermore, we discuss the current limitations of the approach in a zero-sum setting and sketch future work in non-zero-sum settings.

翻译：反应式系统综合旨在自动构建与环境交互的系统的策略。尽管综合方法因避免手动实现而具有显著改变反应式系统开发流程的潜力，但在众多应用场景中仍缺乏高效的合成算法。将系统规约转换为支持策略构建的自动机，在S1S规约长度上具有非初等复杂度，在LTL规约上则呈现双重指数复杂度，这凸显了对高度专业化算法的需求。本文提出一种利用规约单调性特性来减少自动机构建过程中状态空间爆炸的方法。为此，我们引入窗口计数约束，该约束允许对规约进行逐步细化或抽象。在迭代综合过程中，这些窗口计数约束被用于构建表示符合约束行为的过近似或欠近似（取决于计数约束类型）自动机。通过分析前次迭代获胜区域的结果来缩减后续自动机的规模，从而实现整体状态空间爆炸程度的降低。我们展示了零和博弈场景下迭代综合的实现结果作为概念验证。此外，我们讨论了当前方法在零和场景下的局限性，并展望了非零和场景下的未来研究方向。