Abstraction in parameterised Boolean equation systems

S. Cranen, M.W. Gazda, J.W. Wesselink, T.A.C. Willemse

Research output: Book/ReportReportAcademic

82 Downloads (Pure)


We present a general theory of abstraction for a variety of verification problems. Our theory is set in the framework of parameterized Boolean equation systems. The power of our abstraction theory is compared to that of generalised Kripke modal transition systems (GTSs). We show that for model checking the modal µ-calculus, our abstractions can be exponentially more succinct than GTSs and our theory is as complete as the GTS framework for abstraction. Furthermore, we investigate the completeness of our theory for verification problems other than the modal µ-calculus. We illustrate the potential of our theory through case studies using the first-order modal µ-calculus and a real-time extension thereof, conducted using a prototype implementation of a new syntactic transformation for equation systems.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages33
Publication statusPublished - 2013

Publication series

NameComputer science reports
ISSN (Print)0926-4515


Dive into the research topics of 'Abstraction in parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this