# Characterising Probabilistic Alternating Simulation for Concurrent Games

## TL;DR

This paper introduces a new logical framework for characterising probabilistic alternating simulation in concurrent games, providing a sound and complete modal logic that captures the behavior of probabilistic game structures.

## Contribution

It proposes a novel probabilistic distribution-based logic with fixpoints that fully characterises probabilistic alternating simulation, advancing theoretical understanding.

## Key findings

- Sound and complete modal characterisation of probabilistic alternating simulation
- A new logic based on probabilistic distributions for concurrent games
- Extension with fixpoints captures a wide range of properties

## Abstract

Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probabilistic distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also characterises the simulation relation, can express a lot of interesting properties in practical applications.