Movatterモバイル変換

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.