Negotiation as concurrency primitive (Q1731828)

This paper introduces negotiations, a model of concurrency close to Petri nets, with multi-party negotiations as concurrency primitive. The soundness problem consists in deciding if it is always possible for a negotiation to terminate successfully, whatever the current state is. Given a sound negotiation, the summarization problem aims at computing an equivalent one-step negotiation with the same input/output behavior. The soundness and summarization problems can be solved by means of simple algorithms acting on the state space of the negotiation, which, however, face the well-known state explosion problem. Alternative algorithms that avoid the construction of the state space are studied. In particular, reduction rules that simplify a negotiation while preserving the sound/non-sound character of the negotiation and its summary are defined. It is shown that defined rules are complete for the class of weakly deterministic acyclic negotiations, meaning that they reduce all sound negotiations in this class, and only them, to equivalent one-step negotiations. This provides algorithms for both the soundness and the summarization problems that avoid the construction of the state space. The class of deterministic negotiations is studied. The second main result shows that the rules are also complete for this class, even if the negotiations contain cycles. Moreover, an algorithm that completely reduces all sound deterministic negotiations, and only them, in polynomial time is presented.