zbMATH — the first resource for mathematics

Automated verification and strategy synthesis for probabilistic systems. (English) Zbl 1410.68233
Hung, Dang Van (ed.) et al., Automated technology for verification and analysis. 11th international symposium, ATVA 2013, Hanoi, Vietnam, October 15–18, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8172, 5-22 (2013).
Summary: Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, “the minimum probability of the network recovering from a fault in a given time period is above 0.98”. Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methods for automated verification and strategy synthesis for probabilistic systems. Primarily, we focus on the model of Markov decision processes and use property specifications based on probabilistic LTL and expected reward objectives. We also describe how to apply multi-objective model checking to investigate trade-offs between several properties, and extensions to stochastic multi-player games. The paper concludes with a summary of future challenges in this area.
For the entire collection see [Zbl 1291.68023].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Full Text: DOI