In model checking, program correctness on all inputs is verified
by considering the transition system underlying a given program.
In practice, the system can be intractably large.
In property testing, a property of a single input is verified
by looking at a small subset of that input.
We join the strengths of both approaches by
introducing to model checking the notion of probabilistic
abstraction.
We put forth the notion of $eps$-reducibility which is implicit
in many property testers.
Our probabilistic abstraction
associates a set of small random transition systems to a program.
Under some conditions, these transition systems are sufficient
to guarantee that a program approximately decides on all its
inputs a property like bipartiteness, $k$-colorability,
or any first order graph properties of type $existsforall$.
We give a concrete example of an abstraction for a program
which decides bipartiteness.
Finally, we show that abstraction is necessary by
proving an exponential lower bound on OBDDs for
approximate bipartiteness.

In model checking, program correctness on all inputs is verified
by considering the transition system underlying a given program.
In practice, the system can be intractably large.
In property testing, a property of a single input is verified
by looking at a small subset of that input.
We join the strengths of both approaches by
introducing to model checking the notion of probabilistic
abstraction.
We put forth the notion of $\eps$-reducibility which is implicit
in many property testers.
Our probabilistic abstraction
associates a set of small random transition systems to a program.
Under some conditions, these transition systems are sufficient
to guarantee that a program approximately decides on all its
inputs a property like bipartiteness, $k$-colorability,
or any first order graph properties of type $\exists\forall$.
We give a concrete example of an abstraction for a program
which decides bipartiteness.
Finally, we show that abstraction is necessary by
proving an exponential lower bound on OBDDs for
approximate bipartiteness.