Verifying Liveness Properties of Parameterized Systems
<P>
Amir Pnueli (Wezmann)
<P>
 
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.
<P>
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"}.