Skip to Main content Skip to Navigation
Conference papers

PARAM: A Model Checker for Parametric Markov Models

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00650737
Contributor : Wendelin Serwe Connect in order to contact the contributor
Submitted on : Tuesday, January 3, 2012 - 11:45:49 AM
Last modification on : Friday, February 4, 2022 - 3:24:54 AM
Long-term archiving on: : Wednesday, April 4, 2012 - 2:21:17 AM

File

Hans-Hermanns-Wachter-Zhang-10...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00650737, version 1

Citation

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang. PARAM: A Model Checker for Parametric Markov Models. Computer Aided Verification, 22nd International Conference, CAV 2010, Jul 2010, Edinburgh, United Kingdom. pp.660-664. ⟨hal-00650737⟩

Share

Metrics

Record views

284

Files downloads

633