Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

TL;DR

The paper tackles state-space explosion in reactive-systems synthesis by introducing window counting constraints, which impose monotone, sliding-window requirements on how often actions are chosen in a game. It develops an incremental synthesis approach that starts from small counting windows and progressively enlarges them, reusing information from earlier increments to prune the growing automata via situation graphs. A monotonicity theorem underpins the method, enabling safe refinement and guiding when to abandon parts of the search space. The approach supports multiple winning conditions (safety, reachability, Büchi, co-Büchi, parity) and demonstrates significant memory/time savings in zero-sum experiments, with future work aimed at cooperative/environmental settings, new constraint types, symbolic representations, and symmetric systems.

Abstract

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.

Figures (10)

• Figure 1: Small game graph for a two-player game. Circles represent states controlled by $EGO$, diamond-shaped states are controlled by $ALTER$. Transitions are equipped with the actions a player plays when deciding for a transition. For example, $EGO$ can choose in state 3 to play $x$ and $y$ in one turn (leading to state 4) or just play $x$ (and not $y$), which leads to state 2.
• Figure 2: Illustration of the "sliding window"-property of window counting constraints: Each constraint needs to be fulfilled at each part of a play. Actions in $\pi$ played by $EGO$ are highlighted in bold. $\pi$ is a prefix of a play in the game graph shown in Figure \ref{['fig:example_countingConstraints']}.
• Figure 3: Graph for a safety game that cannot be used in a game with the counting constraint "$ALTER$ plays $b$ at least 1 time in 1 turn.". Circles represent states controlled by $EGO$, diamond-shaped states are controlled by $ALTER$. The state colored in gray marks an unsafe state. When the lower subgraph is entered, $A$ cannot fulfill its counting constraint, violating the fourth property in Definition \ref{['def:gameWithCounstraints']}.
• Figure 4: Snippet of a situation graph for the game from Example \ref{['exa:gameWithCountingConstraints']}. A state ("situation") of the game graph is shown as a combination of a state from the original game graph (Figure \ref{['fig:example_countingConstraints']}) with a history that allows to check counting constraint fulfillment in the situation. For better readability, the history is written as table with the name of the counting constraints as header: $C_1 =$ "The player $EGO$ plays $x$ at least $2$ times out of $4$ of its own turns.", $C_2 =$ "The player $EGO$ plays $y$ at least $1$ times out of $5$ of its own turns.", $C_3 =$ "The player $EGO$ plays $y$ at most $2$ times out of $3$ of its own turns.", $C_4 =$ "The player $ALTER$ plays $a \vee b$ at least $1$ time out of $2$ of its own turns.".
• Figure 5: Examples for situations being extensions of other situations. The notation is the same as in Example \ref{['exa:situationgraphExample']} and Figure \ref{['fig:situationgraphExample']}.

Theorems & Definitions (13)

• Definition 2.1: Two-player game graph
• Definition 2.2: Infinite play
• Definition 2.3: Strategy
• Definition 2.4: Winning conditions
• Definition 2.5: Window Counting Constraints
• Example 2.6
• Example 2.8
• Theorem 3.1
• Lemma 3.2
• Example 3.3