Abstraction in fixpoint logic

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

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

5 Citaten (Scopus)
1 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
Pagina's (van-tot)29/1-39
Aantal pagina's39
TijdschriftACM Transactions on Computational Logic
Volume16
Nummer van het tijdschrift4
DOI's
StatusGepubliceerd - 2015

Vingerafdruk Duik in de onderzoeksthema's van 'Abstraction in fixpoint logic'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit