Implicit Real Vector Automata

被引:0
作者
Boigelot, Bernard [1 ]
Brusten, Julien [1 ]
Degbomont, Jean-Francois [1 ]
机构
[1] Univ Liege, Inst Montefiore, B28, B-4000 Liege, Belgium
关键词
D O I
10.4204/EPTCS.39.5
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:63 / 76
页数:14
相关论文
共 22 条
[1]   THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS [J].
ALUR, R ;
COURCOUBETIS, C ;
HALBWACHS, N ;
HENZINGER, TA ;
HO, PH ;
NICOLLIN, X ;
OLIVERO, A ;
SIFAKIS, J ;
YOVINE, S .
THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :3-34
[2]  
ALUR R, 1993, REAL-TIME SYSTEMS SYMPOSIUM: PROCEEDINGS, P2, DOI 10.1109/REAL.1993.393520
[3]  
BERTACCO V, 1997, P INT C COMP AID DES, P78
[4]  
Boigelot B., 2005, ACM Transactions on Computational Logic, V6, P614, DOI 10.1145/1071596.1071601
[5]  
Boigelot B, 1998, LECT NOTES COMPUT SC, V1443, P152, DOI 10.1007/BFb0055049
[6]  
Boigelot B, 1997, LECT NOTES COMPUT SC, V1254, P167
[7]  
Boigelot B, 2009, LECT NOTES ARTIF INT, V5663, P469, DOI 10.1007/978-3-642-02959-2_34
[8]  
Cousot P., 1978, C REC 5 ANN ACM SIGP, P84
[9]  
DILL DL, 1990, LECT NOTES COMPUT SC, V407, P197
[10]  
Ferrante J., 1975, SIAM Journal on Computing, V4, P69, DOI 10.1137/0204006