Sciweavers

Share
LICS
2002
IEEE

Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing

11 years 4 months ago
Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing
istic Abstraction for Model Checking: an Approach Based on Property Testing∗ Sophie Laplante† Richard Lassaigne‡ Fr´ed´eric Magniez§ Sylvain Peyronnet† Michel de Rougemont¶ 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 tion of probabilistic abstraction, and by extending the framework of model checking to include of these abstractions. ractions 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...
Sophie Laplante, Richard Lassaigne, Fréd&ea
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where LICS
Authors Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet, Michel de Rougemont
Comments (0)
books