一句话:提出基于结构分支单元的组合式方法,将含混淆的 Petri 网转换为无混淆网,从而为分布式选择赋予概率语义。
为含混淆与分布式决策的 Petri 网赋予真正并发语义是长期难题,尤其当决策需按概率分布解决时。本文提出组合式方案:递归、静态地把出现网分解为决策位置,称为结构分支单元(s-cell),每个 s-cell 暴露一组称为事务(transaction)的备选。该方法将原网转换为新网:变迁为 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.
@article{paperbot736,
title = {Concurrency and Probability: Removing Confusion, Compositionally},
author = {Roberto Bruni and Hernán Melgratti and Ugo Montanari},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:17)2019}
}