The goal of model checking is to verify the correctness of
a given program, on all of its inputs. The main obstacle,
in many cases, is the intractably large size of the program's
transition system.
Property testing is a randomized method to verify
whether some fixed property holds on individual inputs.
This is done by looking at a small random part of that input.
We join the strengths of both approaches by
introducing a new notion of probabilistic
abstraction, and by extending the framework of model checking to
include the use of these abstractions.
Our abstractions map transition systems associated with large graphs
to small transition systems associated with small random
subgraphs. This reduces the original transition system
to a family of small, even constant-size, transition systems.
We prove that with high probability, ``sufficiently'' incorrect
programs will be rejected ($\eps$-robustness). We also prove
that under a certain condition (exactness), correct programs will
never be rejected (congruence).
Our work applies to programs for graph properties such as
bipartiteness, $k$-colorability,
or any $\exists\forall$ first order graph properties.
Our main contribution is to show how to apply the ideas
of property testing to syntactic programs for such properties.
We give a concrete example of an abstraction for a program
for bipartiteness. Finally, we show that the relaxation
of the test alone does not yield
transition systems small enough to use the standard model checking
method. More specifically, we prove, using methods from communication
complexity, that the OBDD size remains exponential for approximate
bipartiteness.
