We present a new technique for the automatic verification of first order modal μ-calculus formulae on infinite state, data-dependent processes. The use of boolean equation systems for solving the model-checking problem in the finite case is well-studied. We extend this technique to infinite state and data-dependent processes. We describe a transformation of the model checking problem to the problem of solving equation systems, and present a semi-decision procedure to solve these equation systems and discuss the capabilities of a prototype implementing our procedure. This prototype has been successfully applied to many systems. We report on its functioning for the Bakery Protocol.
['Jan Friso Groote', 'Tim A. C. Willemse']
A checker for modal formulae for processes with data