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.
Type de document :
Communication dans un congrès
Tayssir Touili, Byron Cook, Paul Jackson. Computer Aided Verification, 22nd International Conference, CAV 2010, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6174, pp.660-664, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00650737
Contributeur : Wendelin Serwe <>
Soumis le : mardi 3 janvier 2012 - 11:45:49
Dernière modification le : mercredi 11 avril 2018 - 01:54:53
Document(s) archivé(s) le : mercredi 4 avril 2012 - 02:21:17

Fichier

Hans-Hermanns-Wachter-Zhang-10...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Tayssir Touili, Byron Cook, Paul Jackson. Computer Aided Verification, 22nd International Conference, CAV 2010, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6174, pp.660-664, 2010, Lecture Notes in Computer Science. 〈hal-00650737〉

Partager

Métriques

Consultations de la notice

418

Téléchargements de fichiers

428