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

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.