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

TL;DR

This paper extends the PRISM model checker to handle fixed-delay CTMCs with rewards, enabling the synthesis of optimal fixed-delays to minimize expected rewards in probabilistic models.

Contribution

We developed a synthesis algorithm for fixed-delays in fdCTMCs within PRISM, allowing epsilon-optimal delay computation to optimize expected rewards.

Findings

Effective synthesis of fixed-delays demonstrated on practical examples

Extension supports evaluation of expected rewards until target states

Performance evaluation shows practical applicability

Abstract

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.