一句话：证明确定性协商图（等价于自由选择工作流 Petri 网）的健全性、摘要与期望成本等静态分析问题可在 PTIME 内求解。
协商图是类似工作流 Petri 网的并发计算模型。本文研究其确定性片段（等价于广泛使用的自由选择工作流 Petri 网）上的静态分析问题。作者利用该模型的结构性质，给出判定健全性（接近无死锁）的多项式时间算法，并进一步证明对于健全的确定性协商图，计算摘要和期望成本等基本问题也可在 PTIME 内解决。相比一般情形下这些问题为 PSPACE-complete，确定性限制带来显著的复杂度下降，表明该子类对验证具有出人意料的易处理性。
Negotiation diagrams are a model of concurrent computation akin to workflow Petri nets. Deterministic negotiation diagrams, equivalent to the much studied and used free-choice workflow Petri nets, are surprisingly amenable to verification. Soundness (a property close to deadlock-freedom) can be decided in PTIME. Further, other fundamental questions like computing summaries or the expected cost, can also be solved in PTIME for sound deterministic negotiation diagrams, while they are PSPACE-complete in the general case.
@inproceedings{EsparzaMW17,
title = {Static analysis of deterministic negotiations},
author = {Javier Esparza and Anca Muscholl and Igor Walukiewicz},
booktitle = {LICS},
year = {2017},
doi = {10.1109/lics.2017.8005144}
}