CTMCs with Imprecisely Timed Observations

TL;DR

This paper presents a novel method for computing reachability probabilities in labeled continuous-time Markov chains with imprecise timing of observations by unfolding states into an infinite MDP and then abstracting it into a finite model for analysis.

Contribution

It introduces a new approach that handles uncertain timing of observations in CTMCs by formalizing the problem as an infinite MDP and then approximating it with a finite interval MDP for practical computation.

Findings

Method successfully applied to several numerical benchmarks.

Provides a way to upper-bound conditional probabilities in CTMCs.

Discusses challenges and potential improvements for scalability.

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.