PARAM: A Model Checker for Parametric Markov Models

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

76 Citations (Scopus)

Abstract

We present PARAM 1.0, 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 post-process the result function symbolically using for instance computer algebra packages, to derive optimum parameters or to identify worst cases.
Original languageEnglish
Title of host publicationComputer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings
Pages660-664
Number of pages5
DOIs
Publication statusPublished - 2010
Externally publishedYes

Fingerprint

Dive into the research topics of 'PARAM: A Model Checker for Parametric Markov Models'. Together they form a unique fingerprint.

Cite this