Stochastic Parity Games on Lossy Channel Systems

TL;DR

This paper presents an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, focusing on finite-memory strategies and utilizing a finite attractor framework.

Contribution

It introduces a general framework for 2.5-player games with almost-sure parity conditions on infinite graphs, and applies it to lossy channel systems.

Findings

Algorithm for stochastic parity games on lossy channels

Framework for games with finite attractors and almost-sure winning conditions

Characterization of winning states in infinite game graphs

Abstract

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2.5-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.