Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces

Isabelle Mainz
Friday, 27 April, 2018 - 16:00
ULB La Plaine NO, Salle Solvay
Convex polyhedra are of interest in many areas of computer science, in particular for representing reachable sets during symbolic state-space exploration. This work is aimed at developing an efficient data structure for handling such polyhedra, that is closed under intersection and linear transformations, and allows to test inclusion, equality and emptiness. Existing solutions to this problem have several drawbacks: Some representations such as those based on logical formulas are difficult to simplify, which makes them inefficient for handling simple sets constructed by long sequences of manipulations, and data structures based on the double-description method suffer from combinatorial explosion in high-dimensional spaces. Our approach is to represent convex polyhedra using an automaton-like data structure, the Decomposed Convex Polyhedron (DCP). DCPs have the advantage of being canonical, which reduces equality checking to a simple syntactic check, and are able to represent concisely all the convex polyhedra that can be decomposed into a generalized Cartesian product of smaller ones.