Implicit Real Vector Automata

Bernard Boigelot
(Institut Montefiore, B28 Université de Liège B-4000 Liège, Belgium)
Julien Brusten
(Institut Montefiore, B28 Université de Liège B-4000 Liège, Belgium)
Jean-François Degbomont
(Institut Montefiore, B28 Université de Liège B-4000 Liège, Belgium)

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.

In Yu-Fang Chen and Ahmed Rezine: Proceedings 12th International Workshop on Verification of Infinite-State Systems (INFINITY 2010), Singapore, 21st September 2010, Electronic Proceedings in Theoretical Computer Science 39, pp. 63–76.
Published: 28th October 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.39.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org