TY - GEN
T1 - Soundness in negotiations
AU - Esparza, Javier
AU - Kuperberg, Denis
AU - Muscholl, Anca
AU - Walukiewicz, Igor
N1 - Publisher Copyright:
© Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz; licensed under Creative Commons License CC-BY.
PY - 2016/8/1
Y1 - 2016/8/1
N2 - 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 a former paper, 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 provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
AB - 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 a former paper, 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 provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
KW - Concurrency
KW - Negotiations
KW - Soundness
KW - Verification
KW - Workflows
UR - http://www.scopus.com/inward/record.url?scp=85012878362&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CONCUR.2016.12
DO - 10.4230/LIPIcs.CONCUR.2016.12
M3 - Conference contribution
AN - SCOPUS:85012878362
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 27th International Conference on Concurrency Theory, CONCUR 2016
A2 - Desharnais, Josee
A2 - Jagadeesan, Radha
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 27th International Conference on Concurrency Theory, CONCUR 2016
Y2 - 23 August 2016 through 26 August 2016
ER -