Formal Analysis of Electrical Circuit Network Topologies Using Theorem Proving

Electrical circuit networks consist of various electrical components connected in different arrangements that are used to process electrical signals, such as voltages and currents. Moreover, they are widely used in many engineering and physical systems, such as control, embedded and communication systems. In this work, we propose to use higher-order-logic theorem proving for formally analyzing electrical circuit networks using network topology matrices. In particular, we formalize in the Is-abellelHOL theorem prover incidence and circuit (loop) matrices, which are widely used topology matrices. Our formalization is based on modeling the system as a network using the notion of directed graphs that are algebraically represented by matrices. Next, we use this formalization to formally analyze various network topologies, such as Δ-<tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$Y$</tex> and ∏ - <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$L$</tex> topologies, where we perform Kirchhoff's current and voltage laws based analysis in a generic way.