Non-convex polyhedra; Boolean combinations of linear constraints; Data structure
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Brusten, Julien ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Degbomont, Jean-François ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Dép. d'électric., électron. et informat. (Inst.Montefiore)
Language :
English
Title :
Implicit Real Vector Automata
Publication date :
2010
Event name :
12th International Workshop on Verification of Infinite-State Systems
Event place :
Singapore, Singapore
Event date :
September 21th, 2010
Audience :
International
Journal title :
Electronic Proceedings in Theoretical Computer Science
eISSN :
2075-2180
Publisher :
Open Publishing Association, Sydney, Australia
Volume :
39
Pages :
63-76
Peer reviewed :
Peer Reviewed verified by ORBi
Funders :
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)
