@article{REMKE200724,
    Abstract = {We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic stopping criterion, the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.},
    Author = {Remke, Anne and Haverkort, Boudewijn R. and Cloth, Lucia},
    File = {CSL model checking algorithms for QBDs - 1-s2.0-S0304397507004483-main - a.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Keywords = {CSL, Model checking, Infinite-state, Quasi-birth death processes, Continuous-time Markov chains, Uniformization, Transient analysis},
    Note = {Quantitative Aspects of Programming Languages},
    Number = {1},
    Pages = {24-41},
    Title = {CSL model checking algorithms for QBDs},
    URL = {https://www.sciencedirect.com/science/article/pii/S0304397507004483},
    Volume = {382},
    Year = {2007},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397507004483},
    bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2007.05.007},
    date-added = {2022-12-26 21:32:24 +0100},
    date-modified = {2022-12-26 21:32:24 +0100},
    doi = {10.1016/j.tcs.2007.05.007}
}

@article{REMKE200724, Abstract = {We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic stopping criterion, the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.}, Author = {Remke, Anne and Haverkort, Boudewijn R. and Cloth, Lucia}, File = {CSL model checking algorithms for QBDs - 1-s2.0-S0304397507004483-main - a.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {CSL, Model checking, Infinite-state, Quasi-birth death processes, Continuous-time Markov chains, Uniformization, Transient analysis}, Note = {Quantitative Aspects of Programming Languages}, Number = {1}, Pages = {24-41}, Title = {CSL model checking algorithms for QBDs}, URL = {https://www.sciencedirect.com/science/article/pii/S0304397507004483}, Volume = {382}, Year = {2007}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397507004483}, bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2007.05.007}, date-added = {2022-12-26 21:32:24 +0100}, date-modified = {2022-12-26 21:32:24 +0100}, doi = {10.1016/j.tcs.2007.05.007} }