eng
episciences.org
Logical Methods in Computer Science
1860-5974
2018-01-16
Volume 14, Issue 1
Concurrency theory
10.23638/LMCS-14(1:4)2018
3196
journal article
Soundness in negotiations
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.
https://lmcs.episciences.org/3196/pdf
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