Implicit Real Vector Automata

TL;DR

This paper introduces a novel data structure for representing complex non-convex real polyhedra using an implicit encoding of Real Vector Automata, enabling canonical forms, Boolean operations, and efficient membership testing.

Contribution

It presents an original, concise encoding of Real Vector Automata for symbolic representation of non-convex polyhedra, improving efficiency and canonical form.

Findings

Provides a formalism that is closed under Boolean operations

Enables efficient membership testing for complex polyhedra

Offers a canonical representation of non-convex sets

Abstract

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.