Using Acceleration to Compute Parameterized System Refinement

In this paper, we present a verification approach for a class of parameterized systems. These systems are composed of an arbitrary number of similar processes. As in \cite{abdulla99b} we represent the states by regular languages and the transitions by transducers over regular languages. If we can compute a symbolic model by acceleration of the actions, then we can also verify a refinement relation R between the symbolic models. We show that, under some conditions, if R is verified between two symbolic models, then refinement is verified between concrete parameterized systems. Then, we can take advantage the property (safety and PLTL properties) preservation by refinement for their verification.