Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)
arXiv:1405.1841
Abstract
We survey some results on the automatic verification of parameterized programs without identities. These are systems composed of arbitrarily many components, all of them running exactly the same finite-state program. We discuss the complexity of deciding that no component reaches an unsafe state. The note is addressed at theoretical computer scientists in general.
A former version of this paper was published in the Proceedings of STACS 2014. This version corrects two mistakes in Sections 3.3. and 3.4, and some typos