PARAM: A Model Checker for Parametric Markov Models

Ernst Moritz Hahn, Holger Hermanns, Bjorn Wachter, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

84 Citations (Scopus)


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
Subtitle of host publication22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings
ISBN (Electronic)978-3-642-14295-6
ISBN (Print)978-3-642-14294-9
Publication statusPublished - 2010
Externally publishedYes
Event22nd International Conference on Computer Aided Verification, CAV 2010 - Edinburgh, United Kingdom
Duration: 15 Jul 201019 Jul 2010
Conference number: 22

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference22nd International Conference on Computer Aided Verification, CAV 2010
Abbreviated titleCAV 2020
Country/TerritoryUnited Kingdom


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

Cite this