Deriving bisimulations by simplifying partitions

Abstract

In this paper we analyze the problem of transforming partitions in order to satisfy completeness in the standard abstract interpretation framework. 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 the existing notions of completeness, but also with the simplification of domains for completeness (the so called core). Then we show that completeness lies, under the stability form, in two fields of computer science security: abstract non-interference and opacity. © 2008 Springer-Verlag Berlin Heidelberg.