paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Concurrency and Probability: Removing Confusion, Compositionally

并发与概率:组合式消除混淆
LMCS vol.Volume 15, Issue 42019匹配度 2/10 · 该论文研究 Petri 网中并发与概率的形式语义,属于并发理论/形式语义方向,与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接交集。虽然涉及概率,但并非程序分析或 LLM 交叉方向,匹配度较低。引用 1 inbox
Roberto Bruni, Hernán Melgratti, Ugo Montanari
crossref: 2026-09-10

AI 速览

一句话:提出基于结构分支单元的组合式方法,将含混淆的 Petri 网转换为无混淆网,从而为分布式选择赋予概率语义。

为含混淆与分布式决策的 Petri 网赋予真正并发语义是长期难题,尤其当决策需按概率分布解决时。本文提出组合式方案:递归、静态地把出现网分解为决策位置,称为结构分支单元(s-cell),每个 s-cell 暴露一组称为事务(transaction)的备选。该方法将原网转换为新网:变迁为 s-cell 的事务,库所为原网库所并辅以簿记结构。新网无混淆,故冲突备选可施加概率选择,而不相交备选保持纯并发且分布独立。作者通过其构造与 Abbes 与 Benveniste 的递归停止格局之间的紧密对应来验证正确性。其优点是 s-cell 静态、局部且组合地定义,所得网忠实刻画并发。

问题
为含混淆和分布式决策的 Petri 网提供令人满意的真正并发语义,并处理按概率分布解决冲突决策的问题。
方法
通过递归、静态地将出现网分解为结构分支单元(s-cell),再把原网转换为以 s-cell 事务为变迁、无混淆且带辅助簿记的新网。
评估
通过与 Abbes 和 Benveniste 的递归停止格局建立紧密对应来论证构造正确性;新网既支持冲突备选的概率选择,又保持非相交备选的纯并发与独立分布。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}