BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Measuring progress of probabilistic model-checkers
- Franck van Breugel\, York University\, Toronto
DTSTART:20120405T150000Z
DTEND:20120405T160000Z
UID:TALK782AT
URL:/talk/index/782
DESCRIPTION:Verification of the source code of a probabilistic
system by means of an explicit-state model-checke
r is challenging. In most cases\, the probabilisti
c model-checker will run out of memory due to the
infamous state space explosion problem. In this ta
lk\, we introduce the notion of a progress measure
for such a model-checker. The progress measure re
turns a number in the interval [0\, 1]. This numbe
r provides us a quantitative measure of the amount
of progress the model-checker has made with verif
ying a particular linear-time property. The larger
the number\, the more progress the model-checker
has made. In particular\, the progress measure pro
vides a lower-bound of the measure of the set of e
xecution paths that satisfy the property.\n\nJava
PathFinder (JPF) in an explicit-state model-checke
r for Java bytecode. We have extended JPF to a pro
babilistic model-checker. JPF can traverse the sta
te space in different ways\, including depth-first
and breadth-first. With the additional probabilis
tic information available to JPF\, new traversal s
trategies can be added to JPF. We present a few si
mple traversal strategies that take the probabilit
ies into account.\n\nWe have extended JPF so that
it keeps track of the amount of progress it has ma
de with checking properties expressed in a particu
lar fragment of linear temporal logic. We show the
difference in progress of the different traversal
strategies for a few examples.\n\nThis is joint w
ork with Elise Cormie-Bowins and Xin Zhang.
LOCATION:UG40 Computer Science
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR