Linearization of ?CRL specifications

We describe a linearization algorithm for ?CRL processes, similar to the one described in [21] for a subset of the language called parallel pCRL. This algorithm finds its roots in formal language theory: the `grammar' defining a process is transformed into a variant of Greibach Normal Form. Next, any such form is further reduced to linear form, i.e., to an equation that resembles a right-linear, data-parametric grammar. From the other perspective, linear specifications in ?CRL resemble symbolicrepresentations of transition systems, that can be further transformed and analyzed by many of the existing tools and techniques. We aim at proving the correctness of this linearization algorithm. To this end we use an equivalence relation on recursive specifications in ?CRL that is model independent and does not involve an explicit notion of solution.