Computing Publications

Publications Home » More precise partition abstractions

More precise partition abstractions

Harald Fecher, Michael Huth

Conference or Workshop Paper
Eighth International Conference on Verification, Model Checking, and Abstract Interpretation, 14-16 January 2007, Nice, France
January, 2007
Lecture Notes in Computer Science
Volume 4349
Springer Verlag
ISSN 0302-9743

We define, for any partition of a state space, two variants of precision of abstractions that have the partition set as state space. These variants are defined via satisfaction parity games in which the Refuter can replace a concrete state with any state in the same partition before, respectively after, a quantifier or literal move. These games are independent of the kind of abstraction. Our first variant captures the definition of precision given by Shoham & Grumberg, is a special case of the abstraction games by de Alfaro et al., and corresponds to generalized Kripke modal transition systems. Our second variant is then shown to render more precise abstractions in the form of mu-automata without fairness. We discuss the relative tradeoffs of both variants in terms of the size of abstractions, the perceived cost of their synthesis via theorem provers, and the preservation of equations that are valid over concrete models. Finally, we sketch a combination of both abstraction methods.


This is a preliminary version of the actual publication and does not yet reflect the comments of referees.

PDF of full publication (212 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.