Paper Info
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.
Year
DOI
Venue
2010
10.1007/978-3-642-14295-6_56
CAV
Keywords
Field
DocType
result function,optimum parameter,model checker,expensive analysis,multiple individual instantiations,evaluation result,instance computer algebra package,parametric markov model,certain extension,parametric discrete-time markov chain,rational function,markov model,computer algebra
Polynomial,Markov model,Computer science,Markov chain,Symbolic computation,Algorithm,Theoretical computer science,Parametric statistics,Variable-order Markov model,Parametricity,Rational function
Conference
Volume
ISSN
ISBN
6174
0302-9743
3-642-14294-X
Citations 
PageRank 
References 
54
1.52
14
Authors
4
Name
Order
Citations
PageRank
Ernst Moritz Hahn136823.99
Holger Hermanns23418229.22
Björn Wachter332620.09
Lijun Zhang445124.40