Toward parameterized verification of synchronous distributed applications
Sagar Chaki, James Edmondson · 2014
We present preliminary results on parameterized verification of distributed applications that assume a synchronous model of computation. Our theoretical results are negative -- the problem is undecidable even if each node has a single bit of non-determinism and the property is a 1-index safety property. Further, even if each node is completely deterministic, and the property is again a 1-index safety, parameterized verification cannot be solved via the cutoff method. Empirically, we show how to encode such applications as Array-Based Systems and verify them using existing model checkers. We demonstrate this approach on protocols for distributed mutual exclusion and collision avoidance.