This artifact contains an implementation of the approach from the paper "CTMCs with Imprecisely Timed Observations" presented at TACAS 2024. The implementation is written in Python and builds upon the probabilistic model checker Storm. The artifact contains all benchmarks (CTMC models, properties, and evidences) used in the numerical experiments presented in Section 6 of the paper. The artifact allows to reproduce all the results of the numerical experiments, in particular, Table 2 and Figure 6 (in the main paper) and Figure 8 (in the appendix). The artifact is licensed under GPL-3.0 Please see the README within the zip archive on how to obtain, build and run the artifact. Requirements: No special requirements are needed, the artifact works without an internet connection. Building the artifact requires 1-2 hours. Running all experiments requires roughly 4 hours.
Date made available | 28 Dec 2023 |
---|
Publisher | Zenodo |
---|