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

• Autoři: KORENČIAK Ľuboš; ŘEHÁK Vojtěch; FARMADIN Adrian
• Rok publikování: 2016
• Druh: Článek ve sborníku
• Konference: Integrated Formal Methods
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: 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
• Obor: Informatika
• Klíčová slova: CTMC; DSPN; synthesis; timeout; expected reward; PRISM model checker
• Popis: 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.

Související projekty

• Centrum excelence - Institut teoretické informatiky
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity