TY - GEN
T1 - A Probabilistic Logic for Verifying Continuous-time Markov Chains
AU - Guan, Ji
AU - Yu, Nengkun
N1 - Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the probability distribution execution of CTMCs. We define the syntax of CLL on the space of probability distributions. The syntax of CLL includes multiphase timed until formulas, and the semantics of CLL allows time reset to study relatively temporal properties. We derive a corresponding model-checking algorithm for CLL formulas. The correctness of the model-checking algorithm depends on Schanuel’s conjecture, a central open problem in transcendental number theory. Furthermore, we provide a running example of CTMCs to illustrate our method.
AB - A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the probability distribution execution of CTMCs. We define the syntax of CLL on the space of probability distributions. The syntax of CLL includes multiphase timed until formulas, and the semantics of CLL allows time reset to study relatively temporal properties. We derive a corresponding model-checking algorithm for CLL formulas. The correctness of the model-checking algorithm depends on Schanuel’s conjecture, a central open problem in transcendental number theory. Furthermore, we provide a running example of CTMCs to illustrate our method.
UR - https://www.scopus.com/pages/publications/85125029870
U2 - 10.1007/978-3-030-99527-0_1
DO - 10.1007/978-3-030-99527-0_1
M3 - Conference contribution
AN - SCOPUS:85125029870
SN - 9783030995263
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 21
BT - Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
A2 - Fisman, Dana
A2 - Rosu, Grigore
PB - Springer Science and Business Media Deutschland GmbH
T2 - 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022
Y2 - 2 April 2022 through 7 April 2022
ER -