Rescuing Catastrophe Victims by Interactive Markov Chains with Clocks
摘要
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.