On the Formalization of Network Topology Matrices in HOL
This work provides a formal verification tool for engineers and researchers in fields like electrical circuits and communication networks, but it is incremental as it applies existing theorem-proving methods to a specific domain.
The authors tackled the problem of formalizing network topology matrices, such as adjacency and Laplacian matrices, using Higher-Order Logic in the Isabelle/HOL proof assistant, resulting in a verified framework that includes proofs of classical properties and applications like Kron reduction and power dissipation analysis.
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.