Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Linda Feeken, Martin Fränzle

TL;DR

This article presents an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotonicity property of specifications by introducing window counting constraints that allow for step-wise refinement or abstraction of specifications.

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 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.

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

TL;DR

This article presents an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotonicity property of specifications by introducing window counting constraints that allow for step-wise refinement or abstraction of specifications.

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 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.

Paper Structure

This paper contains 6 sections, 1 theorem, 2 equations, 3 figures, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Games with Counting Constraints
  4. Iterated Synthesis with Counting Constraints
  5. Discussion and Future Work
  6. Conclusion

Key Result

Theorem 4.1

Let $G = (S, s_0, S_{EGO}, S_{ALTER}, \Sigma_{EGO}, \Sigma_{ALTER}, \rightarrow, CC_{EGO})$ be a two-player game with counting constraints.

Figures (3)

  • Figure 1: Two-player game graph. States represented as circles are controlled by $EGO$, diamond-shaped states are controlled by $ALTER$. $EGO$ shall fulfill the counting constraint $CC_{min}(EGO, a,1,7)$ ($EGO$ plays $a$ at least one time in 7 turns).
  • Figure 2: Situation graphs for the game in \ref{['fig:smallGameIterationsMatter']} with iteration over $CC_{min}(EGO, a,1,7)$. More than three iterations are not necessary, since there already is a winning strategy for $EGO$ in the third iteration.
  • Figure 3: $ALTER$ can always fulfill the counting constraint $CC_{min}(ALTER, b, 1, 3)$, but can run into a violation for $CC_{min}(ALTER, b, 1, 2)$.

Theorems & Definitions (8)

  • Definition 3.1: Two-player game graph
  • Definition 3.2: Infinite play
  • Definition 3.3: Strategy
  • Definition 3.4: Safety Game
  • Definition 3.5: Window Counting Constraints
  • Definition 3.6: Games with Counting Constraints
  • Theorem 4.1
  • Definition 4.1: Situation Graph