Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modular Attractor Acceleration in Infinite-State Games (Full Version)

Philippe Heim, Rayna Dimitrova

TL;DR

Solving infinite-state reactive games hinges on accelerating symbolic attractor computations; the authors introduce a modular framework that constructs acceleration arguments from simple lemmas into Generalized Acceleration Lemmas (GALs) and a dedicated lemma search to compose them via operators such as intersection, lexicographic union, and chaining. They also introduce enforcement summaries to parameterize and reuse acceleration witnesses across multiple target sets using templates and meta variables. The approach is implemented on top of the Issy tool and evaluated against diverse benchmarks, showing improved scalability and the ability to solve previously intractable cases including Büchi and LTL modulo theories objectives. Overall, modular GALs and enforcement summaries extend the range of solvable infinite-state games and provide a practical path toward scalable reactive synthesis for unbounded data domains.

Abstract

Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.

Modular Attractor Acceleration in Infinite-State Games (Full Version)

TL;DR

Solving infinite-state reactive games hinges on accelerating symbolic attractor computations; the authors introduce a modular framework that constructs acceleration arguments from simple lemmas into Generalized Acceleration Lemmas (GALs) and a dedicated lemma search to compose them via operators such as intersection, lexicographic union, and chaining. They also introduce enforcement summaries to parameterize and reuse acceleration witnesses across multiple target sets using templates and meta variables. The approach is implemented on top of the Issy tool and evaluated against diverse benchmarks, showing improved scalability and the ability to solve previously intractable cases including Büchi and LTL modulo theories objectives. Overall, modular GALs and enforcement summaries extend the range of solvable infinite-state games and provide a practical path toward scalable reactive synthesis for unbounded data domains.

Abstract

Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.
Paper Structure (1 section, 1 figure)

This paper contains 1 section, 1 figure.

Table of Contents

  1. Introduction

Figures (1)

  • Figure 1: Symbolic games $\mathcal{G}_R$ and $\mathcal{G}_B$ for the motivating examples. In both games, $x$ and $y$ are integer state variables, and $i$ and $b$ are input variables with integer and Boolean types, respectively. Additionally, the Büchi game $\mathcal{G}_B$ has an integer state variable $c$ and input variables $i_x$ and $i_y$, which are also integers.