CSL model checking algorithms for QBDs


Remke, Anne and Haverkort, Boudewijn R. and Cloth, Lucia (2007) CSL model checking algorithms for QBDs. Theoretical Computer Science, 382 (1). pp. 24-41. ISSN 0304-3975

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:We present an in-depth treatment of model checking lgorithms 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 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 epresentatives. 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.
Item Type:Article
Copyright:© 2007 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/61957
Official URL:https://doi.org/10.1016/j.tcs.2007.05.007
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 241971