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

TL;DR

This paper introduces a novel technique for solving infinite-state games by using localized attractor computations in sub-games, improving efficiency and scalability over existing methods.

Contribution

It presents the first approach that combines symbolic game-solving with localized attractor computations in sub-games for infinite-state games.

Findings

Outperforms existing techniques in experimental evaluations

Applicable to larger and more complex infinite-state games

Effectively identifies useful sub-games for simplified analysis

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.