Erratum to: Model-checking continuous-time Markov chains by Aziz et al

David N. Jansen

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:…