Abstraction in parameterised Boolean equation systems

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

Research output: Book/ReportReportAcademic

60 Downloads (Pure)

Abstract

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
Volume1301
ISSN (Print)0926-4515

Fingerprint

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

Cite this