一句话:用结构分支单元(s-cell)把 Petri 网静态分解并转换为无混淆网,从而统一刻画并发与概率选择。
为带混淆和分布式决策的 Petri 网赋予真正并发语义是长期难题,尤其当决策需服从概率分布时。本文提出基于结构分支单元(s-cell)的通用方案:递归、静态地将出现网分解为决策位点,每个 s-cell 暴露一组事务作为备选。作者将原网转换为新网,其变迁对应 s-cell 的事务,库所保留原网库所并加入簿记辅助结构。新网无混淆,因而冲突备选可赋予概率选择,不相交备选则保持纯并发且概率分布独立。构造的有效性由与 Abbes 和 Benveniste 递归停止格局的紧密对应保证。s-cell 的定义是静态、局部且组合式的,结果网忠实刻画并发。
Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions. Our solution transforms a given Petri net into another net whose transitions are the transactions of the s-cells and whose places are those of the original net, with some auxiliary structure for bookkeeping. The resulting net is confusion-free, and thus conflicting alternatives can be equipped with probabilistic choices, while nonintersecting alternatives are purely concurrent and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence with the recursively stopped configurations of Abbes and Benveniste. Some advantages of our approach are that: i) s-cells are defined statically and locally in a compositional way; ii) our resulting nets faithfully account for concurrency.