2016/03/10 by Ľuboš Korenčiak, Korenčiak, Ľuboš, Vojtěch Řehák +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Performance (cs.PF) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1603.03252
openalex publication_date 2016/03/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.