Liveness with (0, 1,∞)-counter abstraction

Abstract

We introduce the (0, 1,∞)-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 κ(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)t hat 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 also extended to deal with parameterized systems whose processes may have infinitely many local states, such as the Bakery Algorithm, by choosing few “interesting” state assertions and (0, 1,∞)-counting the number of processes satisfying them.