As mentioned above, one important source of parameterization is the existence of parameter variables in the description of the program. The paper [BHM01] extends the model of context-free processes by an integer parameter, and presents a model checking procedure for such systems. The procedure is used for data flow analysis of recursive programs. The paper [ABLS01] studies model checking for counter automata extended with parametric guards supplied with fairness conditions (see the above paragraph on liveness properties).