Measuring Progress of Probabilistic LTL Model Checking

Elise Cormie-Bowins
Franck van Breugel

Recently, Zhang and Van Breugel introduced the notion of a progress measure for a probabilistic model checker. Given a linear-time property P and a description of the part of the system that has already been checked, the progress measure returns a real number in the unit interval. The real number captures how much progress the model checker has made towards verifying P. If the progress is zero, no progress has been made. If it is one, the model checker is done. They showed that the progress measure provides a lower bound for the measure of the set of execution paths that satisfy P. They also presented an algorithm to compute the progress measure when P is an invariant.

In this paper, we present an algorithm to compute the progress measure when P is a formula of a positive fragment of linear temporal logic. In this fragment, we can express invariants but also many other interesting properties. The algorithm is exponential in the size of P and polynomial in the size of that part of the system that has already been checked. We also present an algorithm to compute a lower bound for the progress measure in polynomial time.

In Herbert Wiklicky and Mieke Massink: Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Tallinn, Estonia, 31 March and 1 April 2012, Electronic Proceedings in Theoretical Computer Science 85, pp. 33–47.
Published: 3rd July 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.85.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org