Zonotopes are becoming an increasingly popular set representation for formal verification techniques. This is mainly due to their efficient representation and their favorable computational complexity of important operations in high-dimensional spaces. In particular, zonotopes are closed under Minkowski addition and linear maps, which can be very efficiently implemented. Unfortunately, zonotopes are not closed under Minkowski difference for dimensions greater than two. However, we present an algorithm that efficiently computes a halfspace representation of the Minkowski difference of two zonotopes. In addition, we present an efficient algorithm that computes an approximation of the Minkowski difference in generator representation. The efficiency of the proposed solution is demonstrated by numerical experiments. These experiments show a reduced computation time in comparison to that when first the halfspace representation of zonotopes is obtained and the Minkowski difference is performed subsequently.
翻译:对于正式的核查技术,Zonotopes正日益成为日益受欢迎的典型代表。这主要是因为它们具有高效率的代表性,而且它们在高维空间的重要操作中具有有利的计算复杂性。特别是,在Minkowski添加和线性地图下,zonotops被关闭,可以非常有效地加以执行。不幸的是,在Minkowski差异下,zonotops没有被关闭,其尺寸大于两个维度。然而,我们提出了一个算法,有效地计算了Minkowski差异的半空代表率。此外,我们提出了一个高效的算法,计算了Minkowski在发电机代表方面的差异的近似值。拟议解决方案的效率通过数字实验得到证明。这些实验显示,与最初获得Zonotope的半空代表制和随后进行Minkowski差异相比,计算时间有所缩短。