Precisely deciding CSL formulas through approximate model checking for CTMCs

The model checking problem of continuous-time Markov chains with respect to continuous-time stochastic logic was introduced and shown to be decidable by Aziz et al. [1], [2] in 1996. Unfortunately, their proof is only constructive, but highly unpractical. Later in 2000, an efficient approximate algorithm was proposed by Baier et al. [3], [5] for a sublogic with binary until. In this paper, we apply transcendental number theory and classical linear algebra to bridge the gap between the precise but unpractical algorithm, and the imprecise but efficient approximate algorithm. We prove that the approximate algorithm in [3], [5] can be used as an off-the-shell tool for a precise model checking algorithm for binary until formulas. Further, we discuss extensions of our results to nested until and continuous-time Markov decision processes.