Revision #1 Authors: Sophie Laplante, Richard Lassaigne, Frederic Magniez, Sylvain Peyronnet, Michel de Rougemont

Accepted on: 1st October 2001 00:00

Downloads: 1724

Keywords:

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.

TR01-051 Authors: Sophie Laplante, Richard Lassaigne, Frederic Magniez, Sylvain Peyronnet, Michel de Rougemont

Publication: 16th July 2001 17:41

Downloads: 2830

Keywords:

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.