Liveness and acceleration in parameterized verification

Abstract

The paper considers the problem of uniform verification of parameterized systems by symbolic model checking, using formulas in FS1S (a syntactic variant of the 2nd order logic WS1S) for the symbolic representation of sets of states. The technical difficulty addressed in this work is that, in many cases, standard model-checking computations fail to converge. Using the tool TLV[P], we formulated a general approach to the acceleration of the transition relations, allowing an unbounded number of different processes to change their local state (or interact with their neighbor) in a single step. We demonstrate that this acceleration process solves the difficulty and enables an efficient symbolic model-checking of many parameterized systems such as mutual-exclusion and token-passing protocols for any value of N, the parameter specifying the size of the system. Most previous approaches to the uniform verification of parameterized systems, only considered safety properties of such systems. In this paper, we present an approach to the verification of iveness properties and demonstrate its application to prove accessibility properties of the considered protocols.