非冗余共享的互补分解
Decomposing Non-Redundant Sharing by Complementation
摘要：
求补是约化积运算的逆运算，是一种系统地寻找抽象域的最小分解的技术。File'和Ranzato通过引入一种计算补数的简单方法来推进现有技术。作为一个应用，他们考虑了从Jacobs和Langen的集合共享域SH中通过互补来提取对共享域PS。然而，由于这个操作的结果仍然是SH，他们得出结论，PS太抽象了。在这里，我们表明，这一结果的来源在于不与PS，但与SH，更准确地说，与SH中包含的冗余信息相对于地面依赖性和对共享。事实上，如果SH的非冗余版本PSD代替SH，则获得适当的分解。为了建立PSD的结果，我们定义了一个一般模式的子域SH，包括PSD和DEF的特殊情况。这揭示了PSD的结构，并揭示了Def和PSD之间自然但意想不到的联系。此外，我们证实的索赔，互补本身是不足以获得真正的最小分解域。这个问题的正确解决方案是首先通过计算域相对于可观察行为的商来去除冗余，然后才通过互补来分解它。
英文摘要：
Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. File' and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen's set-sharing domain SH. However, since the result of this operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH, PSD, is substituted for SH. To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
