2010 | OriginalPaper | Buchkapitel
PARAM: A Model Checker for Parametric Markov Models
verfasst von : Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.