Precisely deciding CSL formulas through approximate model checking for CTMCs

Publication Type:
Journal Article
Journal of Computer and System Sciences, 2017, 89 pp. 361 - 371
Issue Date:
Filename Description Size
1-s2.0-S0022000017300855-main.pdfPublished Version401.81 kB
Adobe PDF
Full metadata record
© 2017 Elsevier Inc. 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.
Please use this identifier to cite or link to this item: