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.

翻译：标记连续时间马尔可夫链（CTMC）描述了受随机时序和部分可观测性影响的系统过程。在运行时监控等应用中，我们必须整合历史观测信息。这些观测的时序至关重要但可能存在不确定性。因此，我们考虑这样一种场景：给定一组称为证据的不精确计时标签序列，研究问题在于计算基于该证据的条件可达概率。我们的核心贡献是提出一种通过将CTMC状态展开为所有可能的证据时序来解决该问题的方法。我们将这种展开形式化为一个马尔可夫决策过程（MDP），其中每个证据时序对应一个调度器。该MDP通常具有无限状态和动作，导致直接分析不可行。因此，我们将连续MDP抽象为有限区间MDP（iMDP），并开发迭代细化方案来界定CTMC中的条件概率上界。我们通过多个数值基准实验验证了该方法的可行性，并讨论了进一步提升性能的关键挑战。