12th International Workshop on Verification of Infinite-State Systems
September 21th, 2010
[en] Non-convex polyhedra ; Boolean combinations of linear constraints ; Data structure
[en] This paper addresses the symbolic representation of non-convex real polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop an original data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of polyhedra, is closed under Boolean operators, and admits an efficient decision procedure for testing the membership of a vector.
Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office ; Grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS)