Negotiations: A Model for Tractable Concurrency.

并发理论致力于研究各种通信原语，如共享变量、点对点FIFO通道、集合点或可靠广播。特别是，对于通过这些原语进行通信的抽象机器的验证问题的复杂性进行了很好的研究。不幸的是，系统大小的最坏情况的复杂性非常高，从PSPACE-Hard到用指数塔表示的下界，甚至是非本原递归函数。最近，我们开始了对一种新的交际原语--谈判的研究。协商是同步和非确定性选择的组合(之所以称为协商，是因为在协商过程中，为了从多个结果中选择一个结果，即进行非确定性选择，许多当事人相遇，即同步)。为了进行我们的研究，我们引入了协商图，这是一个以原子协商为原始的并发模型。该模型接近于1-安全着色Petri网。我们的工作已经确定了该模型的一个子类，称为确定性协商图，它表现出了非常好的性质。特别是，即使模型受到状态爆炸问题的影响，也可以在多项式时间内检查基本属性，如健壮性(类似于没有死锁和活锁的属性)。我们还设计了一种小型程序设计语言，它准确地捕获了合理的确定性协商图。以确定性协商图为出发点，我们建议在保持PSPACE复杂性障碍的同时，研究并发系统日益增长的表达模型。虽然这项工作的动机主要是理论上的，但我们将利用所得到的结果来设计一种用于并行程序的小型程序语言，并结合简单的Hoare逻辑和工具支持来自动生成程序的分布式实现。

Concurrency theory has devoted much effort to thestudy of a large variety of communication primitives, likeshared variables, point-to-point FIFO channels, rendez-vous, or reliable broadcasts. In particular, the complexity of verification problems for abstract machines communicating by means of these primitives is very well studied. Unfortunately,the worst-case complexity in the size of the system is very high, ranging from PSPACE-hard to lower bounds expressed in terms oftower of exponentials, or even non-primitive recursive functions. We have recently initiated the study of a novel communication primitive, called negotiation. Negotiation is a combination of synchronization and nondeterministic choice(the name is due to the fact that in a negotiation a numberof parties meet--i.e., synchronize--in order to select one outof a number of outcomes--i.e., to conduct a nondeterministic choice).In order to conduct our study, we have introduced negotiation diagrams,a concurrency model with atomic negotiations as primitive. The modelis close to 1-safe colored Petri nets. Our work has identified a subclass of the model, called deterministicnegotiation diagrams, that exhibits exceptionally good properties. In particular, even though the model is subject tothe state-explosion problem, fundamental properties like soundness(a property similar to absence of deadlocks and livelocks) can be checked in polynomial time. We have alsodesigned a small programming language which captures exactly the sounddeterministic negotiation diagrams. Taking deterministic negotiation diagrams as starting point, we propose to study increasingly expressive models of concurrent systems,while at the same time remaining below the PSPACE complexity barrier.While the motivation of this work is mostly theoretical,we will use the results to design a small programminglanguage for parallel programs, together with a simple Hoare logic, and tool support to automatically produce distributedimplementations of programs.