Measuring progress of probabilistic model-checkers

Add to your list(s) Download to your calendar using vCal

• Franck van Breugel, York University, Toronto
• Thursday 05 April 2012, 16:00-17:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

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 properties expressed in a particular fragment of linear temporal logic. 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.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.