Driven by a need for modelling and optimising rescue scenarios, we suggest an extension of Interactive Markov Chains that features, first, clocks and clock-dependent transition guards as in Timed Automata (TA) and, second, continuously varying, clock-dependent rates of autonomous transitions. The resulting model, called Interactive Markov Chains with Clocks (IMCC) can be seen as a unification of Hermanns’ and Katoen’s IMCs and Alur’s and Dill’s TA, extending both. IMCCs differ from Sproston’s Probabilistic TA with Clock-Dependent Probabilities in that IMCCs feature autonomous transitions with clock-dependent rates. By their clock-dependent rates, they also extend the mechanisms for computing delay distributions offered by Stochastic Automata and Stochastic Timed Automata. In this note, we motivate the model of IMCCs by an example of a strategy evaluation problem in rescue missions with time-variant death rates, as typical of catastrophe victims, and formalise the model. We discuss an effective approximation for computing time-bounded location reachability probabilities and related expected values in IMCCs.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Rescuing Catastrophe Victims by Interactive Markov Chains with Clocks

  • Martin Fränzle,
  • Rabeaeh Kiaghadi,
  • Paul Kröger

摘要

Driven by a need for modelling and optimising rescue scenarios, we suggest an extension of Interactive Markov Chains that features, first, clocks and clock-dependent transition guards as in Timed Automata (TA) and, second, continuously varying, clock-dependent rates of autonomous transitions. The resulting model, called Interactive Markov Chains with Clocks (IMCC) can be seen as a unification of Hermanns’ and Katoen’s IMCs and Alur’s and Dill’s TA, extending both. IMCCs differ from Sproston’s Probabilistic TA with Clock-Dependent Probabilities in that IMCCs feature autonomous transitions with clock-dependent rates. By their clock-dependent rates, they also extend the mechanisms for computing delay distributions offered by Stochastic Automata and Stochastic Timed Automata. In this note, we motivate the model of IMCCs by an example of a strategy evaluation problem in rescue missions with time-variant death rates, as typical of catastrophe victims, and formalise the model. We discuss an effective approximation for computing time-bounded location reachability probabilities and related expected values in IMCCs.