On some Galois connection based abstractions for the mu-calculus

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Downloads (Pure)

Abstract

In this paper we give some abstractions that preserve sublanguages of the universal part of the branching-time µ-calculus Lµ. We first extend some results by Loiseaux et al. by using a different abstraction for the universal fragments of Lµ which are treated in their work. We show that this leads to a more elegant theoretical treatment and more practical verification methodology. After that, we define an abstraction for a universal fragment of Lµ in which the formulas can contain the -operator only under an even number of negations. The abstraction we propose is inspired by the work of Loiseaux et al., and Kesten and Pnueli. From the former we use the approach based on Galois connections, while from the latter we borrow the idea of "rewriting" the original formula using contracting/expanding abstractions. We argue that, besides removing some unnecessary syntactic restrictions, our approach leads to more compact and practical solutions to the abstraction problems. Keywords: abstraction, property preservation, mu-calculus, model checking.
Original languageEnglish
Title of host publicationFM 2005: Formal Methods (International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings)
EditorsJ. Fitzgerald, I.J. Hayes, A. Tarlecki
Place of PublicationBerlin
PublisherSpringer
Pages366-381
ISBN (Print)978-3-540-27882-5
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
Volume3582
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'On some Galois connection based abstractions for the mu-calculus'. Together they form a unique fingerprint.

Cite this