Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring or calculation of remaining useful life, we must incorporate past observations. The timing of these observations matters but they may be uncertain.

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.

In this talk, I will present a method that solves this problem by (1) unfolding the CTMC into a continuous Markov decision process (MDP), (2) abstracting the continuous MDP into a finite interval MDP and (3) applying an iterative refinement scheme to obtain bounds on the conditional probabilities in the CTMC.

(joint work with Thom Badings, Sebastian Junges, Nils Jansen and Marielle Stoelinga)