Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Localized Attractor Computations for Infinite-State Games (Full Version)

Anne-Kathrin Schmuck, Philippe Heim, Rayna Dimitrova, Satya Prakash Nayak

TL;DR

The paper targets solving infinite-state games for reactive synthesis with unbounded data domains and shows that existing abstraction-based or constraint-based methods struggle with large instances. It introduces localization of attractor computations by identifying small sub-games using permissive strategy templates computed on finite abstractions, and then uses an attractor cache to reuse results during the global solve. Formally, it defines attractor caches, sub-game extraction, and template-based identification of helpful edges, enabling accelerated symbolic reachability via the least fixpoint $ $\llbracket\mathsf{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket d\rrbracket)\rrbracket = \llbracket \mu X. d \lor \mathsf{CPre}_{\llbracket\mathcal{G}\rrbracket,p}(X) \rrbracket$ $. The authors implement a prototype RPG solver (rpg-STeLA) and demonstrate that local caching plus pruning outperforms prior techniques on challenging benchmarks with unbounded state spaces, confirming improved scalability and applicability. Overall, the approach integrates abstraction-driven sub-problems with symbolic acceleration to advance practical synthesis for infinite-state games.

Abstract

Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and exploit the respective results for the given game-solving task are highly desirable. In this paper, we propose the first such technique for infinite-state games. The main idea is to enhance symbolic game-solving with the results of localized attractor computations performed in sub-games. The crux of our approach lies in identifying useful sub-games by computing permissive winning strategy templates in finite abstractions of the infinite-state game. The experimental evaluation of our method demonstrates that it outperforms existing techniques and is applicable to infinite-state games beyond the state of the art.

Localized Attractor Computations for Infinite-State Games (Full Version)

TL;DR

The paper targets solving infinite-state games for reactive synthesis with unbounded data domains and shows that existing abstraction-based or constraint-based methods struggle with large instances. It introduces localization of attractor computations by identifying small sub-games using permissive strategy templates computed on finite abstractions, and then uses an attractor cache to reuse results during the global solve. Formally, it defines attractor caches, sub-game extraction, and template-based identification of helpful edges, enabling accelerated symbolic reachability via the least fixpoint \llbracket\mathsf{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket d\rrbracket)\rrbracket = \llbracket \mu X. d \lor \mathsf{CPre}_{\llbracket\mathcal{G}\rrbracket,p}(X) \rrbracket. The authors implement a prototype RPG solver (rpg-STeLA) and demonstrate that local caching plus pruning outperforms prior techniques on challenging benchmarks with unbounded state spaces, confirming improved scalability and applicability. Overall, the approach integrates abstraction-driven sub-problems with symbolic acceleration to advance practical synthesis for infinite-state games.

Abstract

Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and exploit the respective results for the given game-solving task are highly desirable. In this paper, we propose the first such technique for infinite-state games. The main idea is to enhance symbolic game-solving with the results of localized attractor computations performed in sub-games. The crux of our approach lies in identifying useful sub-games by computing permissive winning strategy templates in finite abstractions of the infinite-state game. The experimental evaluation of our method demonstrates that it outperforms existing techniques and is applicable to infinite-state games beyond the state of the art.
Paper Structure (1 section, 2 figures)

This paper contains 1 section, 2 figures.

Table of Contents

  1. Introduction

Figures (2)

  • Figure 1: Schematic paper outline; contributions highlighted in blue.
  • Figure 2: A reactive program game for a sample-collecting robot with locations ${\mathit{base}, \mathit{move}, \mathit{mine}}$, integer-type program variables ${\mathit{pos}, \mathit{done}, \mathit{req}, \mathit{samp}}$ and input variable ${\mathit{inpReq}}$. We use the following abbreviations: $\mathit{enterBase} ~\widehat{=}~ (\mathit{pos} = 12 \land \mathit{done} = 1)$, $\mathit{atMine} ~\widehat{=}~ (\mathit{pos} = 23)$, $\mathit{haveSamples} ~\widehat{=}~ (a > 0 \lor b > 0)$, $\mathit{enough} ~\widehat{=}~ \mathit{samp} \geq \mathit{req}$, $\mathit{sampleA} ~\widehat{=}~ (\mathit{samp} := \mathit{samp} + a)$, $\mathit{sampleB} ~\widehat{=}~ (\mathit{samp} := \mathit{samp} + b)$, and $\mathit{sampleS} ~\widehat{=}~ (\mathit{samp} := \mathit{samp} + 1)$. In each round of the game, the environment chooses a value for the input ${\mathit{inpReq}}$. Based on guards over program variables and inputs, the game transitions to a black square. The system then chooses one of the possible updates to the program variables, thus determining the next location.