On some Galois connection based abstractions for the Mu-calculus

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. © Springer-Verlag Berlin Heidelberg 2005.