We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. In this context, we study the parameterised coverability problem of a configuration, which consists in determining whether there is an initialnumber of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics.
翻译:我们考虑由多个进程组成的网络,所有进程均执行相同的有限状态协议,并通过同步通信机制进行交互。当某个进程发起同步请求时,另一进程可响应请求,双方据此变更各自的控制状态。本研究聚焦于一种称为"非阻塞"的特殊语义:即便没有进程能响应发起请求的进程,该进程仍可自行改变状态。在此背景下,我们研究配置的参数化覆盖性问题——即判断是否存在初始数量的进程以及一条执行路径,使得最终可达配置不小于给定配置。结果表明,该问题属于EXPSPACE完全问题;若协议的状态集被划分为可发起同步请求的状态与可响应同步请求的状态两类,则可在多项式时间内求解。此外,我们证明在我们的语义环境下,是否存在一条执行路径使得所有进程最终处于终止状态的问题不可判定。需指出的是,上述两个问题在经典同步语义下均可在多项式时间内求解。