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 | |
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 | United Kingdom |
City | Edinburgh |
Period | 15/07/10 → 19/07/10 |