A Probabilistic Logic for Verifying Continuous-time Markov Chains

The execution of a continuous-time Markov chain (CTMC) can be regarded as a continuous class of probability distributions over states. In this paper, we propose a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the execution of CTMCs. We define the syntax of CLL over the space of probability distributions. The syntax of CLL includes multiphase until formulas. 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.