A checker for modal formulae for processes with data

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)
5 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationFormal Methods for Components and Objects (Revised Lectures, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003)
EditorsF.S. Boer, M.M. Bonsangue, S. Graf, W.P. Roever, de
Place of PublicationBerlin
ISBN (Print)3-540-22942-6
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'A checker for modal formulae for processes with data'. Together they form a unique fingerprint.

Cite this