Skip to main content
Top

2018 | OriginalPaper | Chapter

Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces

Authors : Bernard Boigelot, Isabelle Mainz

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This work is aimed at developing an efficient data structure for representing symbolically convex polyhedra. We introduce an original data structure, the Decomposed Convex Polyhedron (DCP), that is closed under intersection and linear transformations, and allows to check inclusion, equality, and emptiness. The main feature of DCPs lies in their ability to represent concisely polyhedra that can be expressed as combinations of simpler sets, which can overcome combinatorial explosion in high dimensional spaces. DCPs also have the advantage of being reducible into a canonical form, which makes them efficient for representing simple sets constructed by long sequences of manipulations, such as those handled by state-space exploration tools. Their practical efficiency has been evaluated with the help of a prototype implementation, with promising results.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
They are also known as NNC (Not Necessarily Closed) polyhedra, or copolyhedra.
 
Literature
2.
go back to reference Avis, D.: A revised implementation of the reverse search vertex enumeration algorithm. Polytopes – Combinatorics and Computation, pp. 177–198. Birkhäuser, Basel (2000) Avis, D.: A revised implementation of the reverse search vertex enumeration algorithm. Polytopes – Combinatorics and Computation, pp. 177–198. Birkhäuser, Basel (2000)
3.
go back to reference Bachem, A., Grötschel, M.: Characterizations of adjacency of faces of polyhedra. Mathematical Programming at Oberwolfach, pp. 1–22. Springer, Berlin (1981) Bachem, A., Grötschel, M.: Characterizations of adjacency of faces of polyhedra. Mathematical Programming at Oberwolfach, pp. 1–22. Springer, Berlin (1981)
4.
go back to reference Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRef Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRef
5.
go back to reference Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410(46), 4672–4691 (2009)MathSciNetCrossRef Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410(46), 4672–4691 (2009)MathSciNetCrossRef
6.
go back to reference Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proceedings of the SMT’10 (2010) Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proceedings of the SMT’10 (2010)
8.
go back to reference Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614–633 (2005)MathSciNetCrossRef Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614–633 (2005)MathSciNetCrossRef
11.
go back to reference Chernikova, N.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Comput. Math. Math. Phys. 5(2), 228–233 (1965)MathSciNetCrossRef Chernikova, N.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Comput. Math. Math. Phys. 5(2), 228–233 (1965)MathSciNetCrossRef
12.
go back to reference Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL’77. pp. 238–252. ACM Press (1977) Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL’77. pp. 238–252. ACM Press (1977)
13.
go back to reference Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the POPL’78. pp. 84–96. ACM (1978) Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the POPL’78. pp. 84–96. ACM (1978)
14.
go back to reference Degbomont, J.F.: Implicit Real-Vector Automata. Ph.D. thesis, Université de Liège (2013) Degbomont, J.F.: Implicit Real-Vector Automata. Ph.D. thesis, Université de Liège (2013)
15.
go back to reference Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)CrossRef Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)CrossRef
17.
go back to reference Singh, G., Püschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the POPL’17, pp. 46–59. ACM (2017) Singh, G., Püschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the POPL’17, pp. 46–59. ACM (2017)
19.
go back to reference Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Methods Syst. Des. 11(2), 157–185 (1997)CrossRef Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Methods Syst. Des. 11(2), 157–185 (1997)CrossRef
22.
go back to reference Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The Double Description Method, pp. 51–74. Princeton University Press, Princeton (1953) Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The Double Description Method, pp. 51–74. Princeton University Press, Princeton (1953)
23.
go back to reference Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1999) Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1999)
Metadata
Title
Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
Authors
Bernard Boigelot
Isabelle Mainz
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_17

Premium Partner