Saving space by fully exploiting invisible transitions

Abstract

Checking that a given finite state program satisfies a linear temporal logic property suffers from a severe space and time explosion. One way to cope with this is to reduce the state graph used for model checking. We present an algorithm for constructing a state graph that is a projection of the program’s state graph. The algorithm maintains the transitions and states that affect the truth of the property to be checked. The algorithm works in conjunction with a partial order reduction algorithm. We show a substantial reduction in memory over current partial order reduction methods, both in the precomputation stage, and in the result presented to a model checker, with a price of a single additional traversal of the graph obtained with partial order reduction. As part of our space-saving methods, we present a new way to exploit Holzmann’s Bit Hash Table, which assists us in solving the revisiting problem.