This is Enea.

Home

Personal Info

Research

Papers

Teaching

About

A New Encoding and Implementation of Not Necessarily Closed Convex Polyhedra (TR)

[Page last updated on "January 13, 2005, 15:31:42".]

Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella

Abstract

Convex polyhedra, commonly employed for the analysis and verification of both hardware and software, may be defined either by a finite set of linear inequality constraints or by finite sets of generating points and rays of the polyhedron. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a vector space having one extra dimension and reuse the tools and techniques already available for closed polyhedra. Previously, this embedding has been designed so that a constant number of constraints and a linear number of generators have to be added to the original NNC specification of the polyhedron. In this paper we explore an alternative approach: while still using an extra dimension to represent the NNC polyhedron by a closed polyhedron, the new embedding adds a linear number of constraints and a constant number of generators. As far as the issue of providing a non-redundant description of the NNC polyhedron is concerned, we generalize the results established in a previous paper so that they apply to both encodings.


Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry.
© Enea Zaffanella
enea.zaffanella@unipr.it

| Home | Personal Info | Research | Papers | Teaching | About