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 (if a winning strategy exists) is nonelementary in the length of the specification in S1S and doubly exponential for LTL, raising the need of highly specialized algorithms. In this article, we present an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotonicity property of specifications. For this, we introduce window counting constraints that allow for step-wise refinement or abstraction of specifications. In an iterative 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 extent. 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规约上则呈双指数级增长，这凸显了对高度专业化算法的需求。本文提出一种利用规约单调性特性来缓解自动机构建过程中状态空间爆炸的方法。为此，我们引入窗口计数约束，该约束支持对规约进行逐步细化或抽象。在迭代综合过程中，这些窗口计数约束被用于构建表示符合约束行为的过近似或欠近似自动机（取决于计数约束类型）。通过分析历史迭代中获胜区域的结果来缩减后续自动机的规模，从而整体降低状态空间爆炸程度。我们以零和博弈场景为例展示迭代综合的实现结果作为概念验证。此外，我们讨论了当前方法在零和场景下的局限性，并展望了在非零和场景下的未来研究方向。