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.

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