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