Modal abstractions in $ \mu $ CRL

We describe a framework to generate modal abstract approximations from process algebraic specifications, written in the language µ-CRL. We introduce a new format for processes specification called Modal Linear Process Equation (MLPE). An MLPE represents all the possible interleavings of the parallel composition of a number of processes. Every transition step may lead to a set of abstract states labelled with a set of abstract actions. We use MLPEs to characterize abstract interpretations of systems and to generate Modal Labelled Transition Systems, in which transitions may have two modalities may and must. We prove that the abstractions are sound for the full action-based µ-calculus. The main parts of the theory have been formalized and proved using the automatic theorem prover PVS. The set of definitions, theorems and proofs composes a reusable framework to formally analyze process specifications.