Verification of the source code of a probabilistic system by means of an explicit-state model-checker is challenging. In most cases, the probabilistic model-checker will run out of memory due to the infamous state space explosion problem. As far as we know, we are the first to introduce the notion of a progress measure for such a model-checker. The progress measure returns a number in the interval [0, 1]. This number captures the amount of progress the model-checker has made towards verifying a particular linear-time property. The larger the number, the more progress the model-checker has made. We prove that the progress measure provides a lower bound of the measure of the set of execution paths that satisfy the property. We also show how to compute the progress measure for checking a particular class of linear-time properties, namely invariants. © 2011 Springer-Verlag.
CITATION STYLE
Zhang, X., & Van Breugel, F. (2011). A progress measure for explicit-state probabilistic model-checkers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6756 LNCS, pp. 283–294). https://doi.org/10.1007/978-3-642-22012-8_22
Mendeley helps you to discover research relevant for your work.