Measuring progress of 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. In this talk, we 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 provides us a quantitative measure of the amount of progress the model-checker has made with verifying a particular linear-time property. The larger the number, the more progress the model-checker has made. In particular, the progress measure provides a lower-bound of the measure of the set of execution paths that satisfy the property.

Java PathFinder (JPF) in an explicit-state model-checker for Java bytecode. We have extended JPF to a probabilistic model-checker. JPF can traverse the state space in different ways, including depth-first and breadth-first. With the additional probabilistic information available to JPF, new traversal strategies can be added to JPF. We present a few simple traversal strategies that take the probabilities into account.

We have extended JPF so that it keeps track of the amount of progress it has made with checking invariants. We show the difference in progress of the different traversal strategies for a few examples.

This is joint work with Elise Cormie-Bowins and Xin Zhang.