Linda Feeken ; Martin Fränzle - Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

lmcs:15441 - Logical Methods in Computer Science, March 31, 2026, Volume 22, Issue 1 - https://doi.org/10.46298/lmcs-22(1:29)2026
Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space ExplosionArticle

Authors: Linda Feeken ; Martin Fränzle

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.


Volume: Volume 22, Issue 1
Secondary volumes: Selected Papers of the 15th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2024)
Published on: March 31, 2026
Accepted on: February 18, 2026
Submitted on: March 31, 2025
Keywords: Logic in Computer Science, 93B50

Consultation statistics

This page has been seen 223 times.
This article's PDF has been downloaded 49 times.