Parametrized Systems, simplifying safety

Consider the classical critical section problem where you have a number of finite state processes, say two, racing for the critical section. You can verify the mutual exclusion property by generating all possible runs of the system, and checking that each visited state verifies the desired property. Consider now a finite, but undefined, number of such processes. You can not afford to visit all possible states for each number N of processes. In order to check mutual exclusion for any such number N, one can use some other methodologies such as Regular Model Checking or abstraction from user given predicates, etc. These methodologies are complex in general. For instance, in Regular Model Checking, Transducers are used to represent the transition relation as a regular relation. The property is verified by iterating the transducer. Some techniques (widening, accelerations) are then used to help the conclusion of the analysis. The techniques may be adapted to some examples and not to others. We introduce a simple, uniform and efficient approximation to automatically prove safety properties for parameterized systems with linear topologies. This method easily verifies examples such as Szymanski's algorithm, Burn's algorithm, Illinois' cache coherence protocol, etc.