无限状态广播网络中覆盖性的参数化验证

具有有限状态进程的广播网络中覆盖性的参数化验证已在多种模型与拓扑下被研究。本文试图建立一种广播网络理论，其中进程可以是良结构转移系统。所得形式化系统称为良结构广播网络。针对各类通信拓扑，我们证明了在静态情形（即网络拓扑不允许改变）下覆盖性的可判定性。我们通过证明对于这些类型的静态通信拓扑，广播网络本身是一个良结构转移系统，从而证明了广播网络中覆盖性的可判定性。我们还给出了一种算法，用于在允许节点间链路重配置时判定良结构广播网络的覆盖性。最后，通过对该算法的微小修改，我们证明了当底层进程为下推自动机时覆盖性的可判定性。