A New Scheme for Memory-Efficient Probabilistic Verification
In verification by explicit state enumeration, for each reachable
state of the protocol being verified the full state descriptor is
stored in a state table. Two probabilistic methods -- bitstate hashing
and hash compaction -- have been proposed in the literature that store
much fewer bits for each state but come at the price of some
probability that not all reachable states will be explored during the
search, and that the verifier may thus produce false positives.
Holzmann introduced bitstate hashing and derived an approximation
formula for the average probability that a particular state is not
omitted during the search, but this formula does not give a bound on
the probability of false positives. In contrast, the analysis for
hash compaction, introduced by Wolper and Leroy and improved upon by
Stern and Dill, yielded a bound on the probability that not even one
state is omitted during the search, thus providing a bound on the
probability of false positives.
In this paper, we propose and analyze a new scheme for probabilistic
verification that is a variation of the improved hash compaction
scheme. The main difference is that a tighter bound on the probability
of false positives is calculated by reasoning about a longest path in
the breadth-first search tree of the reachable state space. In
addition, the new scheme employs ordered hashing to reduce the
omission probability when inserting into the state table. In the
industrial protocols we examined, the new scheme yielded an
exponential reduction in the bound on the probability of false
positives, which enabled a roughly 50% reduction in the number of bits
needed for a compressed state. Furthermore, we propose a memory
efficient way to store the information needed for error trace
generation. The outcomes of experiments using the new scheme
confirmed the analysis.