PPL

Some Details About the Parma Polyhedra Library

Under Construction

The Parma Polyhedra Library provides a number of domains and domain constructors. Currently these are:

the domain of topologically closed, rational convex polyhedra (C polyhedra);
the domain of rational convex polyhedra that are not necessarily closed (NNC polyhedra);
the domain of octagonal shapes;
the domain of bounded-difference shapes;
the domain of boxes;
the domain of grids;
the powerset domain construction;
the pointset powerset domain construction, that can be instantiated for any pointset;
the partially reduced product domain construction, which is parametric on the domains of its components and also on the reduction operator.

This choice of domains and the design of their interface has been influenced by a broad range of applications spanning the analysis and verification of imperative, functional and logic programming languages, synchronous languages and synchronization protocols, real-time and hybrid systems.

About the Domains and their Implementation in the PPL

The implementation of the domain of C polyhedra uses the double description representation. This representation was introduced by T. S. Motzkin et al. [MRTT53]: the description based on the intersection of hyperspaces is complemented by its description as a set of all points constructed from several finite sets of vectors (representing, for instance, points and rays) following certain rules for their combination. In other words, in the first representation, a polyhedron is captured by a finite set (or system) of constraints while, in the second representation, it is characterized by a finite set (or system) of generators.

Some operations on convex polyhedra are more conveniently performed using the first representation. Intersection of two polyhedra, for instance, can be characterized by the union of the respective constraint systems. The convex polyhedral hull of two polyhedra, instead, can be easily seen as the union of the respective systems of generators.

The library converts, automatically and lazily, from one representation to the other. Automatically means that the user does not need to worry about when the conversion should take place. Lazily means that the library tries hard to minimize the number of conversions it will perform and exploit, as far as possible, the conversions that are performed.

To perform the conversion, the library uses an algorithm that was originally proposed by T. S. Motzkin et al. [MRTT53], then rediscovered by N. V. Chernikova [Che65], improved by H. Le Verge [Ver92], further improved by D. K. Wilde [Wil93], K. Fukuda and A. Prodon [FP96], N. Halbwachs, Y.-E. Proy and P. Roumanoff [HPR97], and B. Jeannet (author of the New Polka library).

The double description method assumes the constraints are either equalities or non-strict inequalities and only applies to closed polyhedra. To allow for strict inequalities and hence polyhedra that are not necessarily closed (NNC), the library adopts the approach described by N. Halbwachs, Y.-E. Proy, and P. Raymond in [HPR94]. Here, the addition of an extra dimension to the vector space of the polyhedron is used to encode the closedness of each of its defining hyperspaces.

The generator system that the library uses to describe an NNC polyhedron has, in addition to the finite sets of vectors representing points and rays, a set of vectors representing a subset of its closure points. These are points in the topological closure of the polyhedron but not necessarily in the polyhedron itself. See [BRZH02a] for more details about this representation.

The library includes widening algorithms for the domains of C and NNC polyhedra that are based on the widening introduced by N. Halbwachs in [Hal79]. This widening is also described in [HPR97].

[Page last updated on February 22, 2009, 16:53:36.]