TY - JOUR
T1 - Algorithmic Minimization of Uncertain Continuous-Time Markov Chains
AU - Cardelli, Luca
AU - Grosu, Radu
AU - Larsen, Kim G.
AU - Tribastone, Mirco
AU - Tschaikowski, Max
AU - Vandin, Andrea
N1 - Publisher Copyright:
IEEE
PY - 2023/11/1
Y1 - 2023/11/1
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. Here, we consider uncertain CTMCs (UCTMCs), where rates are assumed to vary nondeterministically with time from bounded continuous intervals. A UCTMC can be, therefore, seen as a specific type of Markov decision process for which the analysis is computationally difficult. To tackle this, we develop a theory of minimization, which generalizes the notion of lumpability for CTMCs. Our first result is a quantitative and logical characterization of minimization. Specifically, we show that the reduced UCTMC model has a macrostate for each block of a partition of the state space, which preserves value functions and logical formulae whenever rewards are equal within each block. The second result is an efficient minimization algorithm for UCTMCs by means of partition refinement. As an application, we show that reductions in a number of CTMC benchmark models are robust with respect to uncertainties in original rates.
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. Here, we consider uncertain CTMCs (UCTMCs), where rates are assumed to vary nondeterministically with time from bounded continuous intervals. A UCTMC can be, therefore, seen as a specific type of Markov decision process for which the analysis is computationally difficult. To tackle this, we develop a theory of minimization, which generalizes the notion of lumpability for CTMCs. Our first result is a quantitative and logical characterization of minimization. Specifically, we show that the reduced UCTMC model has a macrostate for each block of a partition of the state space, which preserves value functions and logical formulae whenever rewards are equal within each block. The second result is an efficient minimization algorithm for UCTMCs by means of partition refinement. As an application, we show that reductions in a number of CTMC benchmark models are robust with respect to uncertainties in original rates.
KW - Benchmark testing
KW - Computational modeling
KW - Markov processes
KW - Minimization
KW - Partitioning algorithms
KW - Transient analysis
KW - Uncertainty
UR - http://www.scopus.com/inward/record.url?scp=85149374029&partnerID=8YFLogxK
U2 - 10.1109/TAC.2023.3244093
DO - 10.1109/TAC.2023.3244093
M3 - Journal article
AN - SCOPUS:85149374029
SN - 0018-9286
VL - 68
SP - 6557
EP - 6572
JO - IEEE Transactions on Automatic Control
JF - IEEE Transactions on Automatic Control
IS - 11
ER -