PARAM
Subproject |
S3 |
Categories |
Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems |
Overview |
PARAM is a tool with the purpose of handling parametric variants of models specified in a variant of the PRISM language. PARAM is capable of computing the unbounded reachability probability for parametric discrete-time Markov chains. Apart from this, it can also handle special classes of Markov decision processes, as well as reachability rewards for Markov reward models. To speed up computations, it can compute the (strong and weak) bisimulation quotient of parametric models. |
E.M. Hahn, T. Han, and L. Zhang. Synthesis for PCTL in parametric Markov decision processes. In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - Third International Symposium, volume 6617 of Lecture Notes in Computer Science, pages 146-161, 2011. G. Calin, P. Crouzen, E.M. Hahn, P. D'Argenio, and L. Zhang. Time-bounded reachability in distributed input/output interactive probabilistic chains. In Jaco van de Pol and Michael Weber, editors, Model Checking Software, 17th International SPIN Workshop, volume 6349 of Lecture Notes in Computer Science (LNCS), pages 193-211, 2010. E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. PARAM: A model checker for parametric Markov models. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, 22nd International Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science (LNCS), pages 660-664, 2010. E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer (STTT), 12:1-17, 2010. E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. In Corina S. Pasareanu, editor, Model Checking Software, 16th International SPIN Workshop, volume 5578 of Lecture Notes in Computer Science (LNCS), pages 88-106, 2009. |
|
Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |