Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)

TL;DR

This paper surveys the complexity of automatically verifying parameterized systems composed of identical finite-state components, focusing on the challenge of ensuring safety without component identities.

Contribution

It provides a comprehensive overview of the known complexity results for the verification of parameterized programs without identities.

Findings

Deciding safety properties is computationally complex.

The survey covers various classes of parameterized systems.

Results highlight the inherent difficulty in verifying infinite-component systems.

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.