On the Formalization of Network Topology Matrices in HOL

TL;DR

This paper formalizes network topology matrices within HOL theorem proving, enabling rigorous verification of properties and relationships among matrices used in modeling electrical, communication, and transportation networks.

Contribution

It introduces a formalization of adjacency, degree, Laplacian, and incidence matrices in Isabelle/HOL, with verified properties and relationships for network analysis.

Findings

Formalization of network matrices in HOL

Verification of classical properties and relationships

Analysis of Kron reduction and power dissipation

Abstract

Network topology matrices are algebraic representations of graphs that are widely used in modeling and analysis of various applications including electrical circuits, communication networks and transportation systems. In this paper, we propose to use Higher-Order-Logic (HOL) based interactive theorem proving to formalize network topology matrices. In particular, we formalize adjacency, degree, Laplacian and incidence matrices in the Isabelle/HOL proof assistant. Our formalization is based on modelling systems as networks using the notion of directed graphs (unweighted and weighted), where nodes act as components of the system and weighted edges capture the interconnection between them. Then, we formally verify various classical properties of these matrices, such as indexing and degree. We also prove the relationships between these matrices in order to provide a comprehensive formal reasoning support for analyzing systems modeled using network topology matrices. To illustrate the effectiveness of the proposed approach, we formally analyze the Kron reduction of the Laplacian matrix and verify the total power dissipation in a generic resistive electrical network, both commonly used in power flow analysis.