Parametrized systems arise naturally in the modeling of protocols. For instance, the specification of a protocol may be parametrized by the number of components which may participate in a given session of the protocol. In such a case, it is interesting to verify the correctness of the protocol, regardless of the number of participants in a particular session. Another source of parameterization, is that the description of the protocol may contain variables whose values may change in different runs of the protocol, such as the sizes of messages, length of time-outs and delays, number of message retransmissions, etc.
The problem of verification of general classes of parametrized systems is undecidable1. Therefore, this task has mainly been devoted to invent methods for enhancing the performance of symbolic reachability analysis in order to achieve termination more often in practical applications.