一句话：重新审视协商健全性判定：确定性协商为NLogSpace完全，无环弱非确定性协商多项式可解，且健全性可助分析竞态等性质。
协商（negotiations）是多方分布式协作的形式化模型，也可视为以同步选择为通信原语的并发模型；健全性要求协商从任意可达状态都能完成。此前工作证明一般健全性判定为Pspace完全，确定性协商在Ptime，并将多项式算法扩展到无环非确定性协商，但未分析运行时间，且中间类复杂度未定。本文第一部分重新审视确定性协商，给出Nlogspace完全判定，改进了原线性空间算法；第二部分证明无环弱非确定性协商的健全性可在多项式时间求解，推广并回答了开放问题；第三部分将技术用于竞态检测及其他经典静态分析问题，表明它们在任意无环确定性协商中难解，但在健全情形下可解。
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In earlier work, Esparza and Desel have shown that deciding soundness of a negotiation is Pspace-complete, and in Ptime if the negotiation is deterministic. They have also extended their polynomial soundness algorithm to an intermediate class of acyclic, non-deterministic negotiations. However, they did not analyze the runtime of the extended algorithm, and also left open the complexity of the soundness problem for the intermediate class. In the first part of this paper we revisit the soundness problem for deterministic negotiations, and show that it is Nlogspace-complete, improving on the earlier algorithm, which requires linear space. In the second part we answer the question left open by Esparza and Desel. We prove that the soundness problem can be solved in polynomial time for acyclic, weakly non- deterministic negotiations, a more general class than the one considered by them. In the third and final part, we show that the techniques developed in the first two parts of the paper can be applied to analysis problems other than soundness, including the problem of detecting race conditions, and several classical static analysis problems. More specifically, we show that, while these problems are intractable for arbitrary acyclic deterministic negotiations, they become tractable in the sound case. So soundness is not only a desirable behavioral property in itself, but also helps to analyze other properties.
@article{paperbot436,
title = {Soundness in negotiations},
author = {Javier Esparza and Denis Kuperberg and Anca Muscholl and Igor Walukiewicz},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
number = {Concurrency theory},
year = {2018},
doi = {10.23638/lmcs-14(1:4)2018}
}