Javier Esparza ; Denis Kuperberg ; Anca Muscholl ; Igor Walukiewicz - Soundness in negotiations

lmcs:3196 - Logical Methods in Computer Science, January 16, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:4)2018
Soundness in negotiationsArticle

Authors: Javier Esparza ; Denis Kuperberg ; Anca Muscholl ; Igor Walukiewicz

    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.


    Volume: Volume 14, Issue 1
    Section: Concurrency theory
    Published on: January 16, 2018
    Accepted on: November 15, 2017
    Submitted on: March 16, 2017
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science,F.1.1,F.1.2,F.3.1,F.3.2

    1 Document citing this article

    Consultation statistics

    This page has been seen 1413 times.
    This article's PDF has been downloaded 308 times.