Precisely deciding CSL formulas through approximate model checking for CTMCs

作者：

Highlights：

• An elegant proof for the decidability for model checking Continuous-time Markov chains.

• A nice implication about the precise algorithm exploiting the approximating algorithm.

• Exploit fundamental properties of transcendental numbers.

摘要

•An elegant proof for the decidability for model checking Continuous-time Markov chains.•A nice implication about the precise algorithm exploiting the approximating algorithm.•Exploit fundamental properties of transcendental numbers.

论文关键词：Continuous-time Markov chains,Decision algorithm for CSL,Transcendental numbers,Approximation algorithm

论文评审过程：Received 30 June 2015, Revised 14 February 2017, Accepted 31 May 2017, Available online 13 June 2017, Version of Record 7 August 2017.

论文官网地址：https://doi.org/10.1016/j.jcss.2017.05.014