PARAM: A Model Checker for Parametric Markov Models

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

doi:10.1007/978-3-642-14295-6_56

PARAM: A Model Checker for Parametric Markov Models

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

96 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 language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings
Publisher	Springer
Pages	660-664
ISBN (Electronic)	978-3-642-14295-6
ISBN (Print)	978-3-642-14294-9
DOIs	https://doi.org/10.1007/978-3-642-14295-6_56
Publication status	Published - 2010
Externally published	Yes
Event	22nd International Conference on Computer Aided Verification, CAV 2010 - Edinburgh, United Kingdom Duration: 15 Jul 2010 → 19 Jul 2010 Conference number: 22

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6174
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Computer Aided Verification, CAV 2010
Abbreviated title	CAV 2020
Country/Territory	United Kingdom
City	Edinburgh
Period	15/07/10 → 19/07/10

Access to Document

10.1007/978-3-642-14295-6_56

Cite this

@inproceedings{be90d5e491a548468ffa2046bd959901,

title = "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.",

author = "Hahn, {Ernst Moritz} and Holger Hermanns and Bjorn Wachter and Lijun Zhang",

year = "2010",

doi = "10.1007/978-3-642-14295-6_56",

language = "English",

isbn = "978-3-642-14294-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "660--664",

booktitle = "Computer Aided Verification",

address = "Germany",

note = "22nd International Conference on Computer Aided Verification, CAV 2010, CAV 2020 ; Conference date: 15-07-2010 Through 19-07-2010",

}

Hahn, EM, Hermanns, H, Wachter, B & Zhang, L 2010, PARAM: A Model Checker for Parametric Markov Models. in Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6174, Springer, pp. 660-664, 22nd International Conference on Computer Aided Verification, CAV 2010, Edinburgh, United Kingdom, 15/07/10. https://doi.org/10.1007/978-3-642-14295-6_56

PARAM: A Model Checker for Parametric Markov Models. / Hahn, Ernst Moritz ; Hermanns, Holger; Wachter, Bjorn et al.
Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Springer, 2010. p. 660-664 (Lecture Notes in Computer Science; Vol. 6174).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - PARAM: A Model Checker for Parametric Markov Models

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Wachter, Bjorn

AU - Zhang, Lijun

N1 - Conference code: 22

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-14295-6_56

DO - 10.1007/978-3-642-14295-6_56

M3 - Conference contribution

SN - 978-3-642-14294-9

T3 - Lecture Notes in Computer Science

SP - 660

EP - 664

BT - Computer Aided Verification

PB - Springer

T2 - 22nd International Conference on Computer Aided Verification, CAV 2010

Y2 - 15 July 2010 through 19 July 2010

ER -

PARAM: A Model Checker for Parametric Markov Models

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this