勘误：Aziz等人的模型检验连续时间马尔可夫链
Erratum to: Model-checking continuous-time Markov chains by Aziz et al
摘要：
本注释纠正了CSL的多重直到运算符的语义和算法之间的差异，如在Pr_{> 0.0025}（a until[1，2] b until[3，4] c）中，文章：模型检验连续时间马尔可夫链，Aziz，Sanwal，Singhal和Brayton，TOCL 1（1），2000年7月，pp. 162-170.
英文摘要：
This note corrects a discrepancy between the semantics and the algorithm of the multiple until operator of CSL, like in Pr_{> 0.0025} (a until[1,2] b until[3,4] c), of the article: Model-checking continuous-time Markov chains by Aziz, Sanwal, Singhal and Brayton, TOCL 1(1), July 2000, pp. 162-170.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
