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.
@article{arxiv.1405.1841,
title = {Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)},
author = {Javier Esparza},
journal= {arXiv preprint arXiv:1405.1841},
year = {2014}
}
Comments
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