paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The complexity of soundness in workflow nets

工作流网中健全性的复杂度
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 该论文研究工作流网健全性判定问题的复杂度,属于 Petri 网/形式验证的纯理论工作;与用户关注的 PL→AI、AI→PL、浮点程序分析、贝叶斯程序分析及 LLM 交叉方向均无直接关联。引用 5 inbox
Michael Blondin, Filip Mazowiecki, Philip Offtermatt
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:确定了工作流网三类健全性判定问题的精确复杂度:经典与结构健全性为 EXPSPACE 完全,广义健全性为 PSPACE 完全。

工作流网是 Petri 网的一种流行变体,用于对业务流程进行形式分析;其核心判定问题围绕健全性:给定初始与最终配置,从每个可达配置都能到达最终配置。本文解决了长期未决的三种主要健全性变体——经典、结构和广义健全性——的复杂度问题。结果表明:经典与结构健全性是 EXPSPACE 完全的,而广义健全性出乎意料地是 PSPACE 完全的,因此在计算上更简单。

问题
工作流网中经典健全性、结构健全性与广义健全性判定问题的精确复杂度此前尚未解决。
方法
对三种健全性变体进行复杂度分析,建立匹配的上下界并证明其完备性。
评估
以复杂度类精确刻画各判定问题:经典与结构健全性为 EXPSPACE 完全,广义健全性为 PSPACE 完全。
原文摘要(Abstract)

Workflow nets are a popular variant of Petri nets that allow for the algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with soundness, where the initial and final configurations are specified. Intuitively, soundness states that from every reachable configuration one can reach the final configuration. We settle the widely open complexity of the three main variants of soundness: classical, structural and generalised soundness. The first two are EXPSPACE-complete, and, surprisingly, the latter is PSPACE-complete, thus computationally simpler.

链接与引用

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

BibTeX
@inproceedings{BlondinMO22,
  title = {The complexity of soundness in workflow nets},
  author = {Michael Blondin and Filip Mazowiecki and Philip Offtermatt},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533341}
}