HOL 中网络拓扑矩阵的形式化
计算机科学中的逻辑
2026-03-27 v1 代数拓扑
摘要
网络拓扑矩阵是图的代数表示，广泛用于建模和分析各种应用，包括电路、通信网络和交通系统。在本文中，我们提出使用基于高阶逻辑（HOL）的交互式定理证明来形式化网络拓扑矩阵。具体而言，我们在 Isabelle/HOL 定理证明器中形式化了邻接矩阵、度矩阵、拉普拉斯矩阵和关联矩阵。我们的形式化基于将系统建模为网络，使用有向图（无权和加权）的概念，其中节点充当系统的组件，加权边捕捉它们之间的互连。然后，我们形式化地验证了这些矩阵的各种经典性质，如索引和度。我们还证明了这些矩阵之间的关系，以便为使用网络拓扑矩阵建模的系统分析提供全面的形式推理支持。为了说明所提出方法的有效性，我们形式化地分析了拉普拉斯矩阵的 Kron 降阶，并验证了一个通用电阻性电网络中的总功率耗散，这两者在潮流分析中都很常用。
引用
@article{arxiv.2603.25682,
title = {On the Formalization of Network Topology Matrices in HOL},
author = {Kubra Aksoy and Adnan Rashid and Osman Hasan and Sofiene Tahar},
journal= {arXiv preprint arXiv:2603.25682},
year = {2026}
}