Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors

KORENČIAK Ľuboš ŘEHÁK Vojtěch FARMADIN Adrian

Year of publication 2016
Type Article in Proceedings
Conference Integrated Formal Methods
MU Faculty or unit

Faculty of Informatics

Citation
Web http://link.springer.com/chapter/10.1007/978-3-319-33693-0_9
Doi http://dx.doi.org/10.1007/978-3-319-33693-0_9
Field Informatics
Keywords CTMC; DSPN; synthesis; timeout; expected reward; PRISM model checker
Description We present a practically appealing extension of the probabilistic model checker PRISM rendering it to handle fixed-delay continuous-time Markov chains (fdCTMCs) with rewards, the equivalent formalism to the deterministic and stochastic Petri nets (DSPNs). fdCTMCs allow transitions with fixed-delays (or timeouts) on top of the traditional transitions with exponential rates. Our extension supports an evaluation of expected reward until reaching a given set of target states. The main contribution is that, considering the fixed-delays as parameters, we implemented a synthesis algorithm that computes the epsilon-optimal values of the fixed-delays minimizing the expected reward. We provide a performance evaluation of the synthesis on practical examples.
Related projects: