Implicit Real Vector Automata
Bernard Boigelot (Institut Montefiore, Belgium), Julien Brusten, (Institut Montefiore, Belgium), Jean-Fran\c{c}ois Degbomont (Institut, Montefiore, Belgium)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
