论文标题
仿真作为逻辑关系
Bisimulation as a Logical Relation
论文作者
论文摘要
我们研究了如何使用逻辑关系技术来表征各种形式的一分化。采用的方法是，每种形式的三拟合均对应于从过渡系统中得出的代数结构，并且总体上结果是，在状态空间$ s $和$ t $的两个过渡系统之间的关系$ r $是一个分配的，并且仅当派生的代数结构是从$ r $ $ r $的逻辑关系中自动产生的。我们表明，这种方法适用于原始的公园 - 米尔纳（Park-Milner）分配，并且扩展到弱分支，分支和半分支分支。本文以讨论概率分配的讨论结束，在这种情况下，情况稍微复杂，部分原因是必须包含不仅仅是关系的双象征。
We investigate how various forms of bisimulation can be characterised using the technology of logical relations. The approach taken is that each form of bisimulation corresponds to an algebraic structure derived from a transition system, and the general result is that a relation $R$ between two transition systems on state spaces $S$ and $T$ is a bisimulation if and only if the derived algebraic structures are in the logical relation automatically generated from $R$. We show that this approach works for the original Park-Milner bisimulation and that it extends to weak bisimulation, and branching and semi-branching bisimulation. The paper concludes with a discussion of probabilistic bisimulation, where the situation is slightly more complex, partly owing to the need to encompass bisimulations that are not just relations.
