Name
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 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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11814771_40 | IJCAR |
Keywords | Field | DocType |
efficient sat solvers,inferring network,family p,parameterized system,system p,uniform verification,successive possible invariants,network invariant,overall search procedure,network invariants,competitive learning algorithm,competitive learning,sat solver,satisfiability | Constraint satisfaction,Parameterized complexity,Heuristic,Search algorithm,Computer science,Boolean satisfiability problem,Algorithm,Finite-state machine,Constraint satisfaction problem,Invariant (mathematics) | Conference |
Volume | ISSN | ISBN |
4130 | 0302-9743 | 3-540-37187-7 |
Citations | PageRank | References |
26 | 1.07 | 26 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olga Grinchtein | 1 | 115 | 7.91 |
| Martin Leucker | 2 | 1639 | 112.68 |
| Nir Piterman | 3 | 1154 | 70.02 |