论文标题
最新的分支双性异性技术
Up-to Techniques for Branching Bisimilarity
论文作者
论文摘要
自从引入行为等价的流程上以来，人们一直在寻找伴随这些等价的有效证明技术。强大的双性异性和弱双性恋都伴随着最新技术的库：证明方法的增强。对于分支双性异性，尚未建立这些结果。我们表明，一种有力的证明技术是通过结合工会的三种技术，直至扩展和到Bloom的BB Cool格式的上下文来实现分支双相的声音。然后，我们提出了一个初步的建议，以在抽象的煤层环境中施放上下文技术的正确性证明，涵盖分支，但也涵盖η，延迟和弱双性恋。
Ever since the introduction of behavioral equivalences on processes one has been searching for efficient proof techniques that accompany those equivalences. Both strong bisimilarity and weak bisimilarity are accompanied by an arsenal of up-to techniques: enhancements of their proof methods. For branching bisimilarity, these results have not been established yet. We show that a powerful proof technique is sound for branching bisimilarity by combining the three techniques of up to union, up to expansion and up to context for Bloom's BB cool format. We then make an initial proposal for casting the correctness proof of the up to context technique in an abstract coalgebraic setting, covering branching but also η, delay and weak bisimilarity.
