In a previous paper, we presented a technique called finite
trace covers, in which a program is represented by a set of partial orders.
We also presented classes of reachability properties that could be checked
in time that is polynomial in the size of the trace cover. A deficiency of
this approach was that it did not reduce the complexity of checking
properties that did not belong to an efficient class.
In this paper, we present a technique called predicate filtering, which
can be used as a state space reduction technique to reduce the complexity
of checking general reachability properties. To verify a property  that
does not belong to one of our efficient property classes, the user can
first specify a weaker property  , which belongs to an efficient class.
The program is filtered through the property  . The result is a set of
partial orders, which can be represented as programs, and contain all the
states that satisfy  , while eliminating most of the states that do not.
Traditional model checking techniques can then be used to verify  on
the reduced program.
In experiments, we verified a leader election protocol by constructing
only one-third as many states as constructed by SPIN using partial order
reduction.