Inferring Network Invariants Automatically

TitleInferring Network Invariants Automatically
Publication TypeConference Paper
Year of Publication2006
AuthorsGrinchtein, O, Leucker, M, Piterman, N
Conference NameProceedings of the 3rd International Joint Conference on Automated Reasoning {(IJCAR'06)}
SeriesLecture Notes in Artificial Itelligence
Volume4130
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.

Bibtex: 
@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}
}
Postscript: