Hostname: page-component-76fb5796d-x4r87 Total loading time: 0 Render date: 2024-04-25T13:27:13.193Z Has data issue: false hasContentIssue false

Decomposing non-redundant sharing by complementation

Published online by Cambridge University Press:  25 March 2002

ENEA ZAFFANELLA
Affiliation:
Department of Mathematics, University of Parma, Italy (e-mail: zaffanella@cs.unipr.it)
PATRICIA M. HILL
Affiliation:
School of Computing, University of Leeds, Leeds, UK (e-mail: hill@comp.leeds.ac.uk)
ROBERTO BAGNARA
Affiliation:
Department of Mathematics, University of Parma, Italy (e-mail: bagnara@cs.unipr.it)

Abstract

Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen's set-sharing domain SH. However, since the result of this operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH, PSD, is substituted for SH. To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

Type
Research Article
Copyright
© 2002 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)