Deriving Bisimulations by Simplifying Partitions

By: Isabella Mastroeni

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy


In this paper we analyze the problem of transforming partitions in order to satisfy completeness in the standard abstract interpretation framework. By using the straightforward characterization of equivalence relations by means of abstract domains, we instantiate the framework for making abstract domains complete to partitions. In order to obtain this, we exploit the relation existing between completeness and the Paige-Tarjan notion of stability, already detected in the particular context of refining partitions for completeness. Here we extend this relation in order to cope not only with both the existing notions of completeness, but also with the simplification of domains for completeness (the so called core). Then we show that completeness is present under the stability form, in two fields of computer science security: abstract non-interference and opacity.
Related papers:
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Refining and compressing abstract domains (ICALP'97, LNCS 1256: 771-781, 1997)
  • Completeness in abstract interpretation: A domain perspective (AMAST'97, LNCS 1349: 231-245, 1997)
  • Complete abstract interpretations made constructive (MFCS'98, LNCS 1450:366-377, 1998)
  • Building Complete Abstract Interpretations in a Linear Logic-based Setting (SAS'98, LNCS, 1998)
  • Making abstract interpretations complete (Journal of the ACM. 47(2):361-416 2000).
  • Incompleteness, Counterexamples and Refinements in Abstract Model-Checking (LNCS 2126, SAS'01,2001)