CS Seminar: Roberto Bagnara, February 26, 2004

Speaker

Prof. Roberto Bagnara,
Dipartimento di Matematica, University of Parma, Italy.

Date and Time

Thursday, February 26, 2004 at 14:30

Place

Sala Riunioni,
Dipartimento di Matematica, Università di Parma, Via D'Azeglio 85/A, I-43100 Parma

Title

Representation and Manipulation of Not Necessarily Closed Convex Polyhedra

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). We propose a generalization of the well-known theorems by Minkowski and Weyl, where the concept of generator of an NNC polyhedron is extended to also account for the closure points of the polyhedron. In particular, we show that any NNC polyhedron can be defined directly by means of an extended generator system, namely, a triple of finite sets containing rays, points and closure points of the polyhedron. We propose two alternative implementations for NNC polyhedra, discussing the relative benefits and how the choice of representation can affect the efficiency of the polyhedral operations. We also provide a novel solution to the issue of providing a non-redundant description of NNC polyhedra.

Contact Person

Roberto Bagnara

[Page last updated on November 04, 2003, 09:50:17.]