Finite Abstractions of Network of Impulsive Systems Using Dissipativity Approach
Abdalla Swikir
TL;DR
The paper tackles the challenge of scalable verification and control for networks of impulsive nonlinear systems by developing a dissipativity-based, compositional framework that uses alternating simulation functions to relate concrete subsystems to finite abstractions. It extends the concept of alternating approximate simulation to interconnected subsystems and provides a theorem showing how local abstractions can be composed into a global abstraction under a matrix-inequality condition that avoids traditional gain constraints. A constructive method for building finite abstractions of impulsive subsystems is presented via sampled-data transition systems, with a Lyapunov-like function ensuring dissipativity and forward completeness, and a resulting alternating simulation function between the finite abstraction and the concrete impulsive system. The approach broadens applicability beyond small-gain conditions, enabling scalable model checking and controller synthesis for large, complex networks of impulsive dynamics.
Abstract
This paper introduces a compositional framework for constructing finite abstractions of nonlinear interconnected impulsive systems using dissipativity-based conditions. Central to our approach is the concept of "alternating simulation functions," which serve to relate the concrete dynamics of impulsive subsystems to their finite abstractions. Dissipativity conditions are employed to ensure the compositionality of the finite abstractions, enabling the representation of complex interconnected systems as compositions of their subsystem abstractions. The methodology relies on incremental passivity properties such as supply rates and storage functions, alongside forward completeness, to construct finite abstractions for individual impulsive subsystems.