Model-checking processes with data

We propose a procedure for automatically verifying properties (expressed in an extension of the modal μ-calculus) over processes with data, specified in μCRL. We first briefly review existing work, such as the theory of μCRL and we discuss the logic, called first order modalμ-calculus in more detail. Then, we introduce the formalism of first order boolean equation systems and focus on several lemmata that are at the basis of the soundness of our decision procedure. We discuss our findings on three non-trivial applications for a prototype implementation of this procedure. The results show that our prototype can deal with quite complex and interesting properties and systems, showing the efficacy of the approach.