Memory Reduction via Delayed Simulation

TL;DR

This paper introduces a method to reduce memory requirements in infinite games by simplifying the game graph beforehand, achieving exponential memory savings for certain specifications.

Contribution

It presents a novel approach to memory reduction in infinite games through game graph reduction prior to strategy construction.

Findings

Exponential memory reduction for request-response specifications

Memory savings for fairness conditions

Pre-strategy graph reduction improves efficiency

Abstract

We address a central (and classical) issue in the theory of infinite games: the reduction of the memory size that is needed to implement winning strategies in regular infinite games (i.e., controllers that ensure correct behavior against actions of the environment, when the specification is a regular omega-language). We propose an approach which attacks this problem before the construction of a strategy, by first reducing the game graph that is obtained from the specification. For the cases of specifications represented by "request-response"-requirements and general "fairness" conditions, we show that an exponential gain in the size of memory is possible.