A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

翻译：封包转换网络的僵局是一种状态,其中一个或多个信息尚未达到其目标,但却无法取得任何进一步的进展。 我们正式确定了在封包转换网络背景下三种不同的僵局概念,我们称之为全球、地方和薄弱的僵局。 我们在这些概念之间建立了确切的关系,并证明它们具有不同僵局的特点。 此外,我们用象征性的模范检查器 nuXmv 来遏制封包转换网络的僵局自由。我们实验性地表明,实施这一办法对于在封包转换网络中找到微妙的僵局是有效的。