Harald Fecher, Michael Huth
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.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.