凸多面体和其他数值抽象的精确连接检测
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions
摘要：
判定两个凸多面体的并集本身是否是凸多面体是多面体计算中的一个基本问题;在约束控制领域以及硬件和软件系统的综合、分析、验证和优化中具有重要应用。然而，在这样的应用领域中，一般凸多面体只是许多所谓的数值抽象中的一个，其范围从（不一定闭合的）凸多面体的受限族到非凸几何对象。因此，我们从一个抽象的角度来解决这个问题：对于广泛的数值抽象，可以建模为有界的联合半格-也就是说，偏序的任何有限的元素集有一个最小的上限-，我们显示的必要和充分条件之间的等价格理论的加入和集理论工会。对于封闭凸多面体的情况下-据我们所知，这是唯一一个已经在文献中研究-我们改进后的最先进的提供一个新的算法，具有更好的最坏情况下的复杂性。其他数值抽象的结果和算法是新的本文。所有的算法都已经实现，实验验证，并在帕尔马多面体库。
英文摘要：
Deciding whether the union of two convex polyhedra is itself a convex polyhedron is a basic problem in polyhedral computations; having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In such application fields though, general convex polyhedra are just one among many, so-called, numerical abstractions, which range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices --that is, partial orders where any finite set of elements has a least upper bound--, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra --which, as far as we know, is the only one already studied in the literature-- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
