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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Hahn, E. M., Hermanns, H., Wachter, B., & Zhang, L. (2010). PARAM: A model checker for parametric Markov models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6174 LNCS, pp. 660–664). https://doi.org/10.1007/978-3-642-14295-6_56
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
