CTMCs with Imprecisely Timed Observations

Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga, Nils Jansen

Research output: Working paperPreprintAcademic

15 Downloads (Pure)


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.
Original languageEnglish
Publication statusPublished - 12 Jan 2024


  • cs.LO


Dive into the research topics of 'CTMCs with Imprecisely Timed Observations'. Together they form a unique fingerprint.
  • CTMCs with Imprecisely Timed Observations

    Badings, T., Volk, M., Junges, S., Stoelinga, M. & Jansen, N., 5 Apr 2024, Tools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part II. Finkbeiner, B. & Kovács, L. (eds.). Springer, p. 258-278 21 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    Open Access
    23 Downloads (Pure)

Cite this