CTMCs with Imprecisely Timed Observations
Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga, Nils Jansen
TL;DR
This work tackles the challenge of computing maximal weighted conditional reachability probabilities for labeled finite-state CTMCs when observed labels occur at imprecisely timed moments. The authors convert the problem into an evidence-aware MDP by unfolding the CTMC over all possible timings of the imprecise evidence, then abstract the resulting infinite MDP into a finite interval-MDP (iMDP) through a timed-partitioning scheme. They establish sound upper and lower bounds on the target probability via a robust, refinement-based analysis on the iMDP, and demonstrate practical effectiveness with numerical benchmarks and a prototype Python tool that integrates with Storm. The approach yields reasonably tight bounds within feasible runtimes and highlights future directions such as improved refinement strategies and efficient handling of consistent schedulers. Overall, the paper provides a principled framework for robustly conditioning CTMCs on uncertain observations and delivering actionable probabilistic bounds for runtime monitoring and reliability analysis.
Abstract
Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute reachability probabilities, which we condition on this evidence. Our key contribution is a method that solves this problem by unfolding the CTMC states over all possible timings for the evidence. We formalize this unfolding as a Markov decision process (MDP) in which each timing for the evidence is reflected by a scheduler. This MDP has infinitely many states and actions in general, making a direct analysis infeasible. Thus, we abstract the continuous MDP into a finite interval MDP (iMDP) and develop an iterative refinement scheme to upper-bound conditional probabilities in the CTMC. We show the feasibility of our method on several numerical benchmarks and discuss key challenges to further enhance the performance.