[KP13] Marta Kwiatkowska and David Parker. Automated Verification and Strategy Synthesis for Probabilistic Systems. In Proc. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of LNCS, pages 5-22, Springer. October 2013. [pdf] [bib] [Provides an overview of strategy synthesis techniques for probabilistic models.]
Downloads:  pdf pdf (441 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Links: [Google] [Google Scholar]
Abstract. 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.