Optimizing Performance of Continuous-Time Stochastic Systems using\n Timeout Synthesis

2014/07/17 by Tomǎš Brázdil, Ľuboš Korenčiak, Brázdil, Tomáš +7
Computer Science · Business, Management and Accounting · #Petri Nets in System Modeling #Formal Methods in Verification #Business Process Modeling and Analysis

paper · pdf · doi:10.48550/arxiv.1407.4777

Abstract

We consider parametric version of fixed-delay continuous-time Markov chains\n(or equivalently deterministic and stochastic Petri nets, DSPN) where\nfixed-delay transitions are specified by parameters, rather than concrete\nvalues. Our goal is to synthesize values of these parameters that, for a given\ncost function, minimise expected total cost incurred before reaching a given\nset of target states. We show that under mild assumptions, optimal values of\nparameters can be effectively approximated using translation to a Markov\ndecision process (MDP) whose actions correspond to discretized values of these\nparameters.\n

Related

• Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
• Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration
• Mean-Payoff Optimization in Continuous-Time Markov Chains with\n Parametric Alarms
• Parameter Synthesis for Markov Models: Faster Than Ever
• Imprecise Continuous-Time Markov Chains