We introduce the (0,1,infinity)-counter abstraction method by which a parameterized system of unbounded size is abstracted into a finite-state system. Assuming that each process in the parameterized system is finite-state, the abstract variables are limited counters which count, for each local state s of a process, the number of processes which currently are in local state s. The counters are saturated at 2, which means that counter(s)=2 whenever 2 or more processes are at state s. The emphasis of the paper is on the derivation of an adequate and sound set of fairness requirements (both weak and strong) which enable proofs of liveness properties of the abstract system, from which we can safely conclude a corresponding liveness property of the original parameterized system. We illustrate the method on few parameterized systems, including Szymanski's Algorithm for mutual exclusion.
The method is then extended to deal with parameterized systems whose processes may have infinitely many local states, such as the Bakery Algorithm. The extension is based on a choice of few interesting and relevant state assertions and then (0,1,infinity)-counting the number of processes satisfying each of these assertions.
14th International Conference on Computer Aided Verification