Symmetry and Completeness in the Analysis of Parameterized Protocols

Parameterization is ubiquitous in programming. A particularly interesting case is that of network protocols, which are parameterized by the number of processes, and are usually highly symmetric, being composed of a number of isomorphic processes. While the correctness of a fixed-size instance may be determined using model checking, Apt and Kozen showed (in 1986) that the parameterized model checking question--whether a protocol satisfies its specification in every instance--is undecidable in general. Despite this negative result, the importance of the question has lead to the design of specialized proof methods that are based on summarizing the behavior of a parameterized system, either in terms of instances up to a small cutoff size, or through a small process invariant. Although several protocols have been successfully analyzed with such methods, it is unknown whether such summarization is always possible. In this paper, it is shown that---after essential modifications- --these proof methods are relatively complete. Completeness implies that summarization is always possible, modulo computability considerations. The completeness arguments are surprisingly simple, and show a tight connection between the existence of cutoffs and inductive invariants for the parameterized system. The paper also presents new algorithms to construct inductive invariants of particular shapes, such as (forall i: p(i)). The algorithms compute the strongest invariant of the given shape, and are therefore complete. They exploit a previously unnoticed connection between inductiveness, small model theorems, and compositional analysis.