## Quantitative verification and strategy synthesis for stochastic games.(English)Zbl 1347.93240

Summary: Design and control of computer systems that operate in uncertain, competitive or adversarial, environments can be facilitated by formal modeling and analysis. In this paper, we focus on analysis of complex computer systems modelled as turn-based $$2\frac{1}{2}$$-player games, or stochastic games for short, that are able to express both stochastic and non-stochastic uncertainties. We offer a systematic overview of the body of knowledge and algorithmic techniques for verification and strategy synthesis for stochastic games with respect to a broad class of quantitative properties expressible in temporal logic. These include probabilistic linear-time properties, expected total, discounted and average reward properties, and their branching-time extensions and multi-objective combinations. To demonstrate applicability of the framework as well as its practical implementation in a tool called PRISM-games, we describe several case studies that rely on analysis of stochastic games, from areas such as robotics, and networked and distributed systems.

### MSC:

 93E03 Stochastic systems in control theory (general) 91A15 Stochastic games, stochastic differential games 93B50 Synthesis problems 90C29 Multi-objective and goal programming

### Software:

GAVS; TuLiP; PRISM-games; EAGLE; QUASY; PRISM; MOCHA; PRALINE; PPL; GIST
Full Text: