历史保持双模拟下的事件结构归约
计算机科学中的逻辑
2014-07-01 v2
摘要
事件结构通过事件及其间的依赖关系来表示并发过程,从而对因果性和冲突等行为关系进行建模。自素事件结构提出以来,已涌现出多种具有不同行为关系的事件结构变体,因而其表达能力也各不相同。使用表达能力更强的事件结构的一个潜在优势在于,相较于素事件结构中使用的事件数量,它能以更紧凑的形式表示相同的行为。因此,本文探讨了在一种著名的等价概念——历史保持双模拟(history preserving bisimulation)下,保持行为不变的同时减小事件结构规模的问题。具体而言,我们研究了素事件结构的两种推广形式:第一种称为非对称事件结构,其依赖于一种非对称的冲突关系;第二种称为流事件结构,支持一种析取因果性形式。更具体地,我们描述了在保持原始行为的前提下,将事件结构中的一组事件折叠为单个事件所需满足的条件。连续应用此折叠操作可得到最小规模的事件结构。然而,折叠操作的应用顺序可能导致不同的最小规模事件结构。这一现象对将最小规模事件结构作为行为的规范表示的潜在应用产生了负面影响。
引用
@article{arxiv.1403.7181,
title = {Reduction of Event Structures under History Preserving Bisimulation},
author = {Abel Armas-Cervantes and Paolo Baldan and Luciano Garcia-Bañuelos},
journal= {arXiv preprint arXiv:1403.7181},
year = {2014}
}
备注
23 pages