Rational Verification for Probabilistic Systems

Understand

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium.

• Previous work in this area has largely focussed on deterministic systems.
• In this paper, we develop the theory and algorithms for rational verification in probabilistic systems.
• We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments.