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.
@InProceedings{esparza:LIPIcs.STACS.2014.1, author = {Esparza, Javier}, title = {{Keeping a Crowd Safe: On the Complexity of Parameterized Verification}}, booktitle = {31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)}, pages = {1--10}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-65-1}, ISSN = {1868-8969}, year = {2014}, volume = {25}, editor = {Mayr, Ernst W. and Portier, Natacha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.1}, URN = {urn:nbn:de:0030-drops-44985}, doi = {10.4230/LIPIcs.STACS.2014.1}, annote = {Keywords: Parameterized verification, automata theory} }
Feedback for Dagstuhl Publishing