On Probabilistic Alternating Simulations

TL;DR

This paper introduces probabilistic alternating simulation relations for probabilistic game structures, enabling the analysis of property preservation in probabilistic alternating-time temporal logic, with potential applications in system verification.

Contribution

It defines new probabilistic simulation relations for game structures and studies their property preservation, extending existing frameworks to probabilistic settings.

Findings

Probabilistic alternating simulation preserves probabilistic ATL properties.

Probabilistic alternating forward simulation offers a sound basis for system refinement.

The relations generalize classical simulation concepts to probabilistic game models.

Abstract

This paper presents simulation-based relations for probabilistic game structures. The first relation is called probabilistic alternating simulation, and the second called probabilistic alternating forward simulation, following the naming convention of Segala and Lynch. We study these relations with respect to the preservation of properties specified in probabilistic alternating-time temporal logic.