PROPhESY

PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. We present PROPhESY, a tool for analyzing parametric Markov chains (MCs). It can compute a rational function (i.e., a fraction of two polynomials in the model parameters) for reachability and expected reward objectives. Our tool outperforms state-of-the-art tools and supports the novel feature of conditional probabilities. PROPhESY supports incremental automatic parameter synthesis (using SMT techniques) to determine “safe” and “unsafe” regions of the parameter space. All values in these regions give rise to instantiated MCs satisfying or violating the (conditional) probability or expected reward objective. PROPhESY features a web front-end supporting visualization and user-guided parameter synthesis. Experimental results show that PROPhESY scales to MCs with millions of states and several parameters.


References in zbMATH (referenced in 13 articles )

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

  1. Benouhiba, Toufik: A multi-level refinement approach for structural synthesis of optimal probabilistic models (2021)
  2. Junges, Sebastian; Katoen, Joost-Pieter; Pérez, Guillermo A.; Winkler, Tobias: The complexity of reachability in parametric Markov decision processes (2021)
  3. Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination (2020)
  4. Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh: Exact quantitative probabilistic model checking through rational search (2020)
  5. Ouadjaout, Abdelraouf; Miné, Antoine: Quantitative static analysis of communication protocols using abstract Markov chains (2019)
  6. Bart, Anicet; Delahaye, Benoît; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  7. Bortolussi, Luca; Silvetti, Simone: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models (2018)
  8. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  9. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  10. 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)
  11. Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido: Smoothed model checking for uncertain continuous-time Markov chains (2016)
  12. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: \textttSMT-RAT: an open source \textttC++ toolbox for strategic and parallel SMT solving (2015)
  13. Katoen, Joost-Pieter: Probabilistic programming: a true verification challenge (2015)