Model-checking processes with data

We propose a procedure for automatically verifying properties (expressed in an extension of the modal A-calculus) over processes with data, specified in mu CRL. We first briefly review existing work, such as the theory of mu CRL and we discuss the logic, called first order modal g-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. (c) 2004 Elsevier B.V. All rights reserved.