分离性与双模拟的关系
Relating Apartness and Bisimulation
AI总结：
本文提出分离性作为双模拟的对偶概念，通过证明系统推导元素分离，并分别针对弱双模拟和分支双模拟定义相应分离性，同时在范畴论中证明其初始代数性质。
摘要：
集合范畴上函子的余代数的双模拟可以通过关系范畴中提升函子的余代数来描述。最终余代数由此引出余归纳原理，该原理指出两个双模拟的元素是相等的。对于多项式函子，这导致了众所周知的描述。在本文中，我们研究“分离性”的对偶概念。直观上，如果存在一种正面的方式来区分两个元素，则它们是分离的。换句话说：两个元素是分离的当且仅当它们不是双模拟的。由于分离性是一种归纳性概念，由最小不动点描述，我们可以给出一个证明系统，以推导出两个元素是分离的。该证明系统具有推导规则，并且两个元素是分离的当且仅当存在关于这一事实的有限推导（使用这些规则）。我们以两种不同的方式研究分离性与双模拟。首先，对于带静默（tau）步的标记转换系统上的弱双模拟形式，我们定义了一个对应于弱双模拟的分离性概念，以及另一个对应于分支双模拟的分离性概念。分离性规则可用于表明标记转换系统的两个状态不是分支双模拟的。为了支持标记转换系统上的分离性观点，我们用分支分离性的术语表述了分支双模拟的若干众所周知的性质并证明了它们。其次，我们也研究更一般的范畴情形，并表明确实，分离性是双模拟性在精确的范畴意义上的对偶：分离性是一个初始代数，并引出归纳原理。在这一类比中，我们包含了幂集函子，它为进程理论中的非确定性选择提供了语义。
英文摘要：
A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
