View source for Publications/laplante.07.tocl

{{Publication
| published = true
| date = 2005-11-21
| authors = Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet, Michel de Rougemont
| title = Probabilistic abstraction for model checking: an approach based on property testing
| journal = ACM Transactions on Computational Logic
| lrdeprojects = APMC
| volume = 8
| number = 4
| abstract = The goal of model checking is to verify the correctness of a given program, on all 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, 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 (soundness). Our work applies to programs for graph properties such as bipartiteness, k-colorabilityor any existsforall 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.
| lrdenewsdate = 2005-11-21
| type = article
| id = laplante.07.tocl
| bibtex = 
@Article<nowiki>{</nowiki>	  laplante.07.tocl,
  author	= <nowiki>{</nowiki>Sophie Laplante and Richard Lassaigne and Fr\'ed\'eric
		  Magniez and Sylvain Peyronnet and Michel de Rougemont<nowiki>}</nowiki>,
  title		= <nowiki>{</nowiki>Probabilistic abstraction for model checking: an approach
		  based on property testing<nowiki>}</nowiki>,
  journal	= <nowiki>{</nowiki>ACM Transactions on Computational Logic<nowiki>}</nowiki>,
  year		= 2007,
  month		= aug,
  volume	= 8,
  number	= 4,
  abstract	= <nowiki>{</nowiki>The goal of model checking is to verify the correctness of
		  a given program, on all 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, 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 (soundness). 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.<nowiki>}</nowiki>
<nowiki>}</nowiki>

}}