Verifying Liveness Properties of Parameterized Systems

Amir Pnueli (Wezmann)

Parameterized systems are one of the most manageable classes of infinite-state systems, because they often provide a succinct and highly symmetric symbolic representation of the underlying program. Therefore, they have been extensively studied as a testbed for methods of verifying infinite-state systems. Most of the proposed approaches to the uniform verification of parameterized systems are based on abstraction.

Typically, abstraction methods have been mostly applied to the verification of Safety Properties. In this talk, we will survey several diverse approaches which also allow the establishment of liveness properties of parameterized systems. Among these approaches, we will include: 1. A general framework for data-abstraction which abstracts the system jointly with an arbitrary LTL property. 2. The extension of this framework by augmenting the system with a progress monitor, prior to abstraction. 3. Using Network Invariants which abstract liveness as well as safety. 4. Counter-Abstraction, in which we count how many processes have a particular local state, and then abstract the counters to the 3-valued range: {0, 1, and "2 and above"}.