通过补集分解非冗余共享
摘要:用附加操作的逆运算套用方法是一种系统地寻找抽象域的最小分解的技术。File'和Ranzato通过引入一种计算补集的简单方法,推进了这个领域的技术水平。作为一种应用,他们考虑了从Jacobs和Langen的集合共享域SH中通过补充得到的配对共享域PS的提取。然而,由于这个操作的结果仍然是SH,他们得出结论PS对此来说太抽象。我们在这里展示的结果表明,这个结果的源头不在于PS,而是在于SH,并且更确切地说,是在于SH中关于地面依赖性和配对共享的冗余信息。实际上,如果用非冗余版本的SH,PSD替代SH,就可以得到适当的分解。为了证明PSD的结果,我们定义了SH子域的一个通用模式,其中包括PSD和Def作为特殊情况。这为PSD的结构提供了新的视角,并揭示了Def和PSD之间的自然但意外的联系。此外,我们证明了仅靠补充无法获得真正的最小域分解。解决这个问题的正确方法是首先通过计算与可观察行为相关的域的商取除冗余,然后再通过补充进行分解。
作者:Enea Zaffanella, Patricia M. Hill and Roberto Bagnara
论文ID:cs/0101025
分类:Programming Languages
分类简称:cs.PL
提交时间:2007-05-23