Precisely deciding CSL formulas through approximate model checking for CTMCs

Publication Type:
Journal Article
Citation:
Journal of Computer and System Sciences, 2017, 89 pp. 361 - 371
Issue Date:
2017-11-01
Full metadata record
Files in This Item:
Filename Description Size
1-s2.0-S0022000017300855-main.pdfPublished Version401.81 kB
Adobe PDF
© 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: