Abstraction in parameterised Boolean equation systems

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

Onderzoeksoutput: Boek/rapportRapportAcademic

83 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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's33
StatusGepubliceerd - 2013

Publicatie series

NaamComputer science reports
ISSN van geprinte versie0926-4515


Duik in de onderzoeksthema's van 'Abstraction in parameterised Boolean equation systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit