Output details

Automatic verification of competitive stochastic systems

<10>This paper introduces novel automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. They are modelled as turn-based stochastic multi-player games. We introduce a temporal logic for expressing quantitative properties of stochastic multi-player games, and give algorithms for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker. This is the first work on probabilistic temporal logics for games with thorough verification algorithms and implementations. It has found applications in, e.g., energy management in Microgrids, collective decision making for autonomous systems. The article is an extended version of the paper in the top conference TACAS'12. We were invited to submit an extended version to LMCS, but we published the paper in FMSD.