SOUNDNESS IN NEGOTIATIONS
SOUNDNESS IN NEGOTIATIONS
复制标题
DOI：
10.23638/lmcs-14(1:4)2018
复制
发表时间：
2018-01-01
影响因子：
0.6
通讯作者：
Walukiewicz, Igor
中科院分区：
文献类型：
--
作者：
Esparza, Javier;Kuperberg, Denis;Walukiewicz, Igor
谈判是描述多方分布合作的形式主义。另外，它们可以被视为与同步选择的并发模型作为通信原始的。设计的谈判必须是合理的，这意味着，无论其当前状态如何，谈判仍然可以完成。在较早的工作中，Esparza和Desel表明，确定谈判的健全性是PSPACE的完整性，如果谈判是确定性的，则在PTIME中。他们还将其多项式声音算法扩展到了中间的无环，非确定性谈判。但是，他们没有分析扩展算法的运行时间，并且还打开了中级级别的声音问题的复杂性。在本文的第一部分，我们重新审视了确定性谈判的声音问题，并表明它是Nlogspace - 完整，改进了早期的算法，该算法需要线性空间。在第二部分中，我们回答了Esparza和Desel剩下的问题。我们证明，可以在多项式时间内解决稳健问题的无环，弱的非确定性谈判，这是比他们所考虑的更一般的阶级。在第三部分也是最后一部分中，我们证明了在的前两个部分中开发的技术本文可以应用于合理性以外的分析问题，包括检测种族条件的问题以及几个经典的静态分析问题。更具体地说，我们表明，尽管这些问题对于任意的无环确定性谈判是棘手的，但它们在声音案例中变得可拖延。因此，健全不仅是理想的行为属性本身，而且还有助于分析其他属性。
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.