A Progress Measure For Explicit-State Probabilistic Model-Checkers

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.