PARAM: A Model Checker for Parametric Markov Models. 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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination (2020)
  2. Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh: Exact quantitative probabilistic model checking through rational search (2020)
  3. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  4. Bart, Anicet; Delahaye, Benoît; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  5. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  6. Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
  7. Cubuktepe, Murat; Jansen, Nils; Junges, Sebastian; Katoen, Joost-Pieter; Papusha, Ivan; Poonawala, Hasan A.; Topcu, Ufuk: Sequential convex programming for the efficient verification of parametric MDPs (2017)
  8. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  9. Delahaye, Benoît: Consistency for parametric interval Markov chains (2015)
  10. Tati, Bharath Siva Kumar; Siegle, Markus: Parameter and controller synthesis for Markov chains with actions and state labels (2015)
  11. Bartocci, Ezio; Liò, Pietro; Merelli, Emanuela; Paoletti, Nicola: Multiple verification in complex biological systems: the bone remodelling case study (2012)
  12. Ferrer Fioriti, Luis María; Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn: Variable probabilistic abstraction refinement (2012)
  13. Bartocci, Ezio; Grosu, Radu; Katsaros, Panagiotis; Ramakrishnan, C. R.; Smolka, Scott A.: Model repair for probabilistic systems (2011)
  14. Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn; Zhang, Lijun: PARAM: a model checker for parametric Markov models (2010) ioport