Bisimulation from open maps
Bisimulation from open maps
复制标题
DOI：
10.1006/inco.1996.0057
复制
发表时间：
1996-06-15
影响因子：
1
通讯作者：
Winskel, G
中科院分区：
文献类型：
--
作者：
Joyal, A;Nielsen, M;Winskel, G
提出了对分配的抽象定义。它使得可以在一系列不同模型中进行一致模拟的统一定义，以用于类别的平行计算。例如，考虑了示例，过渡系统，同步树，具有独立性的过渡系统（培养皿网的抽象）和标记的事件结构。在过渡系统上，抽象的定义很容易专门研究米尔纳的强分型。在事件结构上，它解释并导致了Rabinovitch和Traktenbrot以及Van Glabeek和Goltz的历史保护分合的加强。在（前）托普斯（Pre）托普斯（Topos）中出现在Joyal和Moerdijk的作品中，带来了一个新型号，并在Pomset类别上进行预示，将标记的事件结构的类别完全嵌入，并在其上嵌入了一个新模型，并将其带到（前）topos中的开放地图。忠实。为了表明其承诺，这种新的预伐模型具有“改进”操作员。一般方法产生了逻辑，普遍的轩尼诗 - 米勒纳逻辑，这是一般性仿真概念的特征。 （c）1996 Academic Press，Inc。
An abstract definition of bisimulation is presented. It makes possible a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets), and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a strengthening of the history-preserving bisimulation of Rabinovitch and Traktenbrot and van Glabeek and Goltz. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has ''refinement'' operators. The general approach yields a logic, generalising Hennessy-Milner logic, which is characteristic for the generalised notion of bisimulation. (C) 1996 Academic Press, Inc.