Negotiation as concurrency primitive
Negotiation as concurrency primitive
复制标题
DOI：
10.1007/s00236-018-0318-9
复制
发表时间：
2019-03-01
期刊：
影响因子：
0.6
通讯作者：
Hoffmann, Philipp
中科院分区：
文献类型：
--
作者：
Desel, Joerg;Esparza, Javier;Hoffmann, Philipp
本文介绍了谈判，这是一种接近培养皿网的并发模型，多方谈判作为并发性原始。我们研究两个基本分析问题。合理性问题在于决定是否始终可以成功终止，无论当前状态是什么。考虑到合理的谈判，摘要问题旨在计算具有相同输入/输出行为的等效单步谈判。可以通过在谈判的状态空间上的简单算法来解决稳健性和摘要问题，然而，这些算法面临着众所周知的状态爆炸问题。我们研究避免国家空间构建的替代算法。特别是，我们定义了简化谈判的简化规则，同时保留了谈判的声音/非声音特征及其摘要。在第一个结果中，我们表明，对于弱确定的无环谈判的类别，我们的规则是完整的，这意味着它们减少了此类中的所有声音谈判，而仅仅是等效的一步谈判。这为避免构建状态空间的稳健性和摘要问题提供了算法。然后，我们研究确定性谈判的类别。我们的第二个主要结果表明，即使谈判包含周期，此类规则也已完成。此外，我们提出了一种算法，该算法完全降低了所有声音确定性谈判，并且仅在多项式时间内。
This paper introduces negotiations, a model of concurrency close to Petri nets, with multi-party negotiations as concurrency primitive. We study two fundamental analysis problems. 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. We study alternative algorithms that avoid the construction of the state space. In particular, we define reduction rules that simplify a negotiation while preserving the sound/non-sound character of the negotiation and its summary. In a first result we show that our 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 problem that avoid the construction of the state space. We then study the class of deterministic negotiations. Our second main result shows that the rules are also complete for this class, even if the negotiations contain cycles. Moreover, we present an algorithm that completely reduces all sound deterministic negotiations, and only them, in polynomial time.