Inferring Network Invariants Automatically
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 that searches systematically for a
network invariant satisfying a given safety property.
The search is based on algorithms for learning finite automata due
to Angluin and Biermann.
We optimize the search by combining both algorithms for improving
successive 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.