@inproceedings{41cbbcd512554b18aec86612d302db4e,
title = "A checker for modal formulae for processes with data",
abstract = "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.",
author = "J.F. Groote and T.A.C. Willemse",
year = "2004",
doi = "10.1007/978-3-540-30101-1\_10",
language = "English",
isbn = "3-540-22942-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "223--239",
editor = "F.S. Boer and M.M. Bonsangue and S. Graf and \{Roever, de\}, W.P.",
booktitle = "Formal Methods for Components and Objects (Revised Lectures, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003)",
address = "Germany",
}