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

Kurzfassung

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, raising the need of highly specialized algorithms. In this paper we introduce a work-in-progress approach on how to reduce this state space explosion in the construction of this automaton by using an iterating algorithm. We introduce window counting constraints that allow for step-wise strengthening or weakening of specifications. In each iteration, a graph is constructed while using the analysis results of the previous iterations. If a state is known to be in the winning region of a previous iteration (or known to be lost, depending on the used constraint), successors of this state do not need to be considered in the current situation, reducing the extend of the state space explosion. We present the implementation results of the iterated synthesis for a zero-sum game setting as proof of concept. Furthermore, we discuss the limitations of the approach in a zero-sum setting and sketch future work in non-zero-sum settings.