Abstract
This work describes a data structure, the Implicit Real-Vector Automaton (IRVA), suited for representing symbolically polyhedra, i.e., regions of n-dimensional space defined by finite Boolean combinations of linear inequalities. IRVA can represent exactly arbitrary convex and non-convex polyhedra, including features such as open and closed boundaries, unconnected parts, and non-manifold components. In addition, they provide efficient procedures for deciding whether a point belongs to a given polyhedron, and determining the polyhedron component (vertex, edge, facet, …) that contains a point. An advantage of IRVA is that they can easily be minimized into a canonical form, which leads to a simple and efficient test for equality between represented polyhedra. We also develop an algorithm for computing Boolean combinations of polyhedra represented by IRVA.
This work is partially supported by the Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office, and by the grants 2.4607.08 and 2.4545.11 of the Belgian Fund for Scientific Research (F.R.S.-FNRS).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bieri, H., Nef, W.: Elementary Set Operations with d-Dimensional Polyhedra. In: Noltemeier, H. (ed.) CG-WS 1988. LNCS, vol. 333, pp. 97–112. Springer, Heidelberg (1988)
Boigelot, B., Bronne, L., Rassart, S.: An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 167–177. Springer, Heidelberg (1997)
Boigelot, B., Brusten, J., Degbomont, J.-F.: Implicit real vector automata. In: Proc. INFINITY. Electronic Proceedings in Theoretical Computer Science, vol. 39, pp. 63–76 (2010)
Boigelot, B., Brusten, J., Leroux, J.: A Generalization of Semenov’s Theorem to Automata Over Real Numbers. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 469–484. Springer, Heidelberg (2009)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic 6(3), 614–633 (2005)
Bournez, O., Maler, O., Pnueli, A.: Orthogonal Polyhedra: Representation and Computation. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 46–60. Springer, Heidelberg (1999)
Brusten, J.: On the sets of real vectors recognized by finite automata in multiple bases. Ph.D. thesis, University of Liège (2011)
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Hachenberger, P., Kettner, L., Mehlhorn, K.: Boolean operations on 3D selective Nef complexes: Data structure, algorithms, optimized implementation and experiments. Comput. Geom. 38(1-2), 64–99 (2007)
Halbwachs, N., Raymond, P., Proy, Y.E.: Verification of Linear Hybrid Systems by Means of Convex Approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994)
Hopcroft, J.: An n logn algorithm for minimizing states in a finite automaton. Tech. rep., Stanford (1971)
Le Verge, H.: A note on Chernikova’s algorithm. Tech. rep., IRISA, Rennes (1992)
Löding, C.: Efficient minimization of deterministic weak ω-automata. Information Processing Letters 79(3), 105–109 (2001)
Requicha, A.A.G.: Representations for rigid solids: Theory, methods, and systems. ACM Comput. Surv. 12(4), 437–464 (1980)
Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of constraint programming. Elsevier (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Brusten, J., Degbomont, JF. (2012). Automata-Based Symbolic Representations of Polyhedra. In: Dediu, AH., Martín-Vide, C. (eds) Language and Automata Theory and Applications. LATA 2012. Lecture Notes in Computer Science, vol 7183. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28332-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-28332-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28331-4
Online ISBN: 978-3-642-28332-1
eBook Packages: Computer ScienceComputer Science (R0)