Solving Stochastic B\"uchi Games on Infinite Arenas with a Finite Attractor

TL;DR

This paper presents a method for solving stochastic B"uchi games on infinite arenas with a finite attractor, providing a fixpoint characterization of winning strategies and proving decidability in certain probabilistic systems.

Contribution

It introduces a fixpoint approach for solving stochastic B"uchi games on infinite arenas with finite attractors, enabling decidability results for probabilistic lossy channel systems.

Findings

Fixpoint characterization of winning sets

Decidability of stochastic B"uchi games on probabilistic lossy channels

Applicable to infinite probabilistic arenas with finite attractors

Abstract

We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized B\"uchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems.