Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor

Abstract

We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi 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.

In Proceedings QAPL 2013, arXiv:1306.2413

References in corpus (5)

• Multiply-Recursive Upper Bounds with Higman's Lemma
• Qualitative Reachability in Stochastic BPA Games
• Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties
• On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems
• The Parametric Ordinal-Recursive Complexity of Post Embedding Problems

Cited by in corpus (1)

• Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond