Model Checking Parameterized Systems

We consider the model-checking problem for a particular class of parameterized systems: systems that consist of arbitrary numbers of components. The task is to show correctness regardless of the number of components. The term parameterized refers to the fact that the size of the system is a parameter of the verification problem. Examples of parameterized systems include mutual exclusion algorithms, bus protocols, networking protocols, cache coherence protocols, web services, and sensor networks. In this chapter, we will give four examples of techniques that have been used (among many others) for the verification of parameterized systems.