The Regular model checking framework was advocated by the paper [KMM+01] as a uniform framework for the analysis of parametrized systems. The idea of regular model checking is to perform symbolic reachability analysis, using regular sets as a symbolic representation of the state space of the parametrized system. Examples of parametrized systems which can be analyzed in this manner are systems consisting of homogeneous finite-state processes connected in a linear of ring-formed topology.
A major problem in the use of regular model checking is that standard reachability analysis algorithms are in general not guaranteed to terminate. Several papers in the project are therefore devoted to developing acceleration procedures for making the algorithm converge more often in practical applications.
One such an approach [Tou01] is based on widening, in the spirit of the techniques used in abstract interpretation 2. The paper studies widening techniques for regular languages and uses this for accelerating fixpoint computations in regular model checking.
Another approach reported in [DLS01] defines an equivalence relation on states and then collapses equivalent states into order to enhance the performance of the reachability algorithm. The equivalence is based on a novel behavioral equivalence on states based on past and future bisimulations.
The paper [Mai01] adopts a slightly different approach. More precisely, it characterizes a subclass of parameterized systems for which the reachability algorithm is always guaranteed to terminate. The subclass is sufficiently wide to cover existing results for token rings and broadcast protocols.
The paper [BMT01] considers regular model checking using a subclass of regular languages, called Alphabetic Pattern Constraints (APC). In contrast to regular languages, APCs are closed under permutation rewriting, which is a common operation in the description of many classes of parametrized systems. Computing closures under permutations can be seen in this setting as applying meta-transitions in order to accelerate the calculation of the whole reachability set of a system.