Inferring Network Invariants Automatically
| Title | Inferring Network Invariants Automatically |
| Publication Type | Conference Paper |
| Year of Publication | 2006 |
| Authors | Grinchtein, O, Leucker, M, Piterman, N |
| Conference Name | Proceedings of the 3rd International Joint Conference on Automated Reasoning {(IJCAR'06)} |
| Series | Lecture Notes in Artificial Itelligence |
| Volume | 4130 |
| Abstract | Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is a system that abstracts the composition of every number of copies of P running in parallel. If there is such a network invariant, by reasoning about it, uniform verification with respect to the family P[1] || ... || P[n] can be carried out. In this paper, we propose a procedure searching systematically for a network invariant satisfying a given safety property. The search is optimized using a combination of Angluin's and Biermann's learning/inference algorithms for improving successively possible invariants. We also show how to reduce the learning problem to SAT, allowing efficient SAT solvers to be used, which turns out to yield a very competitive learning algorithm. The overall search procedure finds a minimal such invariant, if it exists. |
@inproceedings {GrinchteinLP06,
title = {Inferring Network Invariants Automatically},
booktitle = {Proceedings of the 3rd International Joint Conference on Automated Reasoning {(IJCAR{\textquoteright}06)}},
series = {Lecture Notes in Artificial Itelligence},
volume = {4130},
year = {2006},
abstract = {Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is a system that abstracts the composition of every number of copies of P running in parallel. If there is such a network invariant, by reasoning about it, uniform verification with respect to the family P[1] || ... || P[n] can be carried out. In this paper, we propose a procedure searching systematically for a network invariant satisfying a given safety property. The search is optimized using a combination of Angluin{\textquoteright}s and Biermann{\textquoteright}s learning/inference algorithms for improving successively possible invariants. We also show how to reduce the learning problem to SAT, allowing efficient SAT solvers to be used, which turns out to yield a very competitive learning algorithm. The overall search procedure finds a minimal such invariant, if it exists.},
author = {Olga Grinchtein and Martin Leucker and Nir Piterman}
}
