Abstraction in fixpoint logic

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

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)
1 Downloads (Pure)

Abstract

We present a theory of abstraction for the framework of parameterised Boolean equation systems, a first-order fixpoint logic. Parameterised Boolean equation systems can be used to solve a variety of problems in verification. We study the capabilities of the abstraction theory by comparing it to an abstraction theory for 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 irrespective of the encoded decision problem. 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 parameterised Boolean equation systems.
Original languageEnglish
Pages (from-to)29/1-39
Number of pages39
JournalACM Transactions on Computational Logic
Volume16
Issue number4
DOIs
Publication statusPublished - 2015

Fingerprint Dive into the research topics of 'Abstraction in fixpoint logic'. Together they form a unique fingerprint.

  • Cite this