Measuring Progress of Probabilistic LTL Model Checking

TL;DR

This paper extends the concept of progress measures in probabilistic model checking to a broader class of properties expressed in a fragment of linear temporal logic, providing algorithms for their computation.

Contribution

It introduces algorithms to compute progress measures for positive LTL formulas, expanding the applicability of progress measures in probabilistic verification.

Findings

Algorithm for positive LTL formulas is exponential in property size.

Algorithm for lower bound is polynomial in system size.

Progress measure provides a quantifiable progress indicator in probabilistic model checking.

Abstract

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.