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

Ľuboš Korenčiak, Vojtěch Řehák, Adrian Farmadin

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 e…