A Lattice-Theoretical View of Strategy Iteration

TL;DR

This paper introduces a general lattice-theoretical framework for strategy iteration applicable to a broad class of problems, including energy games and probabilistic automata, providing new algorithms and techniques.

Contribution

It formalizes strategy iteration over complete lattices using MV-chains and develops novel algorithms for non-expansive fixpoint functions, extending previous work on simple stochastic games.

Findings

Developed algorithms for strategy iteration on lattices.

Applied methods to energy games and probabilistic automata.

Provided two techniques: from above and from below.

Abstract

Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min-, respectively, max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.