TY - GEN
T1 - Lumpability for Uncertain Continuous-Time Markov Chains
AU - Cardelli, Luca
AU - Grosu, Radu
AU - Larsen, Kim Guldstrand
AU - Tribastone, Mirco
AU - Tschaikowski, Max
AU - Vandin, Andrea
PY - 2021
Y1 - 2021
N2 - The assumption of perfect knowledge of rate parameters in continuous-time Markov chains (CTMCs) is undermined when confronted with reality, where they may be uncertain due to lack of information or because of measurement noise. In this paper we consider uncertain CTMCs, where rates are assumed to vary non-deterministically with time from bounded continuous intervals. This leads to a semantics which associates each state with the reachable set of its probability under all possible choices of the uncertain rates. We develop a notion of lumpability which identifies a partition of states where each block preserves the reachable set of the sum of its probabilities, essentially lifting the well-known CTMC ordinary lumpability to the uncertain setting. We proceed with this analogy with two further contributions: a logical characterization of uncertain CTMC lumping in terms of continuous stochastic logic; and a polynomial time and space algorithm for the minimization of uncertain CTMCs by partition refinement, using the CTMC lumping algorithm as an inner step. As a case study, we show that the minimizations in a substantial number of CTMC models reported in the literature are robust with respect to uncertainties around their original, fixed, rate values.
AB - The assumption of perfect knowledge of rate parameters in continuous-time Markov chains (CTMCs) is undermined when confronted with reality, where they may be uncertain due to lack of information or because of measurement noise. In this paper we consider uncertain CTMCs, where rates are assumed to vary non-deterministically with time from bounded continuous intervals. This leads to a semantics which associates each state with the reachable set of its probability under all possible choices of the uncertain rates. We develop a notion of lumpability which identifies a partition of states where each block preserves the reachable set of the sum of its probabilities, essentially lifting the well-known CTMC ordinary lumpability to the uncertain setting. We proceed with this analogy with two further contributions: a logical characterization of uncertain CTMC lumping in terms of continuous stochastic logic; and a polynomial time and space algorithm for the minimization of uncertain CTMCs by partition refinement, using the CTMC lumping algorithm as an inner step. As a case study, we show that the minimizations in a substantial number of CTMC models reported in the literature are robust with respect to uncertainties around their original, fixed, rate values.
U2 - 10.1007/978-3-030-85172-9_21
DO - 10.1007/978-3-030-85172-9_21
M3 - Article in proceeding
SN - 978-3-030-85171-2
T3 - Lecture Notes in Computer Science
SP - 391
EP - 409
BT - Quantitative Evaluation of Systems
PB - Springer
T2 - International Conference on Quantitative Evaluation of Systems
Y2 - 23 August 2021 through 27 August 2021
ER -