Probabilistic Model Checking
Christel Baier · NATO science for peace and security series. D, Information and communication security · 2016
Probabilistic model checking is a fully automated method for the quantitative system analysis against temporal logic specifications. This article provides an overview of the main model-checking concepts for finite-state discrete-time Markov chains.