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...

• Type: Conference
• Year: 2002
• Where: LICS
• Authors: Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet, Michel de Rougemont
• Keywords: Automated Reasoning, LICS 2002, Model Checking, Program’s Transition System, Transition Systems