Although regular model checking is a powerful technique, there are several classes of parameterized systems whose behaviors cannot be captured using regular languages. The paper [FP01] considers symbolic model checking using classes of languages more expressive than the regular languages and provides model checking of non-regular parameterized systems (using classes of context-free languages)
Moreover, in many cases, the processes in a parametrized network are infinite-state because of unbounded or parametrized data structures.
The paper [AJ01] considers timed networks, a class of parametrized systems, where the individual components operate on real-valued clocks (and hence not finite-state). The model checking algorithm presented in the paper is used to verify a parametrized version of the well-known Fischer's protocol.
In [BSBL01], a method based on combining a deductive approach with abstraction techniques and finite-state model-checking is presented in order to deal with a class of multi-dimensional parametrized systems. This method is shown to be applicable to the verification of systems such as group membership or distributed shared memory consistency protocols where each processes in the network maintains a structure ranging over the set of participating processes.