CTMCs with Imprecisely Timed Observations

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

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

23 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication30th 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
EditorsBernd Finkbeiner, Laura Kovács
PublisherSpringer
Pages258-278
Number of pages21
ISBN (Electronic)978-3-031-57249-4
ISBN (Print)978-3-031-57248-7
DOIs
Publication statusPublished - 5 Apr 2024
Event30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024 - Luxembourg City, Luxembourg
Duration: 6 Apr 202411 Apr 2024
Conference number: 30

Conference

Conference30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024
Abbreviated titleTACAS 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period6/04/2411/04/24

Keywords

  • cs.LO

Fingerprint

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., 12 Jan 2024, ArXiv.org.

    Research output: Working paperPreprintAcademic

    Open Access
    File
    15 Downloads (Pure)

Cite this