网络验证系统的可达矩阵

摘要

网络验证系统将网络转发状态处理为原子谓词，并将网络路由表压缩到原子谓词索引集中。网络中所有节点对之间的传递闭包是根据所述原子谓词和所述原子谓词索引集计算的，以为相应节点递归地生成所述网络的节点可达性矩阵Mn，根据所述节点可达性矩阵生成所述网络的可达报告。所述可达报告可用于对所述网络进行动态编程。所述计算得到的节点可达性矩阵Mn：在所述节点可达性矩阵Mn的对角线上的任何元素不是空集时，识别所述网络中的环路，并且在所述节点可达性矩阵Mn的一行中的所有元素包括空集时，识别所述网络中的黑洞。所述节点可达性矩阵Mn可以通过仅重新计算受更新影响的元素来更新。