具有非阻塞会合的参数化网络的安全性分析

我们考虑由执行相同有限状态协议并通过会合机制进行通信的进程组成的网络。当一个进程请求会合时，另一个进程可以响应它，二者相应地改变其控制状态。我们在此关注一种称为非阻塞的特定语义，即请求会合的进程即使没有其他进程能够响应，也可以改变其状态。在此背景下，我们研究配置的参数化可覆盖问题，该问题旨在确定是否存在初始进程数以及一次执行能够到达一个大于给定配置的配置。我们证明该问题是 EXPSPACE-完全的；若协议被划分为两组状态（进程可从中请求会合的状态，以及可从中响应会合的状态），则该问题可在多项式时间内求解。我们还证明了在我们的语境下，存在将全部进程带入终态的执行这一问题是不可判定的。而这两个问题在经典会合语义下均可在多项式时间内求解。