We describe a linearization algorithm for parallel pCRL processes similar to the one implemented in the linearizer of the mcrl Toolset. 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 emph{linear form, i.e., to an equation that resembles a right-linear, data-parametric grammar. We aim at proving the correctness of this linearization algorithm. To this end we define an equivalence relation on recursive specifications in mcrl that is model independent and does not involve an explicit notion of solution.

Requirements/Specifications (acm D.2.1), Software/Program Verification (acm D.2.4), Formal Definitions and Theory (acm D.3.1), Language Constructs and Features (acm D.3.3), Semantics of Programming Languages (acm F.3.2), Expressions and Their Representation (acm I.1.1)
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Grammars and rewriting systems (msc 68Q42), Abstract data types; algebraic specification (msc 68Q65), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Groote, J.F, Ponse, A, & Usenko, Y.S. (2000). Linearization in parallel pCRL. Software Engineering [SEN]. CWI.