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 userguided parameter synthesis. Experimental results show that PROPhESY scales to MCs with millions of states and several parameters.
CITATION STYLE
Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., … Ábrahám, E. (2015). PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9206, pp. 214–231). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_13
Mendeley helps you to discover research relevant for your work.