PARAM: A Model Checker for Parametric Markov Models
In Computer Aided Verification, 22nd International Conference (CAV)
, pages 660-664, Springer
, Lecture Notes in Computer Science 6174, 2010.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-14295-6_56
Abstract. We present PARAM, a model checker for parametric discrete-time
Markov chains (PMCs). PARAM can evaluate temporal properties of PMCs and
certain extensions of this class. Due to parametricity, evaluation results are
polynomials or rational functions. By instantiating the parameters in the
result function, one can cheaply obtain results for multiple individual
instantiations, based on only a single more expensive analysis. In addition,
it is possible to postprocess the result function symbolically using for
instance computer algebra packages, to derive optimum parameters or to
identify worst cases.