论文部分内容阅读
将编排映射为Peer(参与者),是对编排进行可实现性分析的第1个步骤.现有文献提出的映射方法未考虑参与者中τ对行为的影响,无法确保编排与参与者间的行为一致性.以Petri网作为形式化基础,提出了一种能够保持编排与参与者间行为一致的映射方法,允许:(1)通过动作映射,将交互式Petri网定义的编排映射为带τ的交互式Petri网;(2)提出了4条τ删除规则,用以对带τ的交互式Petri网中的τ进行有选择的删除;(3)将编排与参与者间的行为一致性问题规约为检验两个交互式Petri间是否满足弱互模拟的问题,并证明