A model checking framework for linear time invariant switching systems using structural systems analysis

This paper introduces the concept of structural hybrid systems to address, as a particular case, the model checking problem of switching (possible large scale) linear time invariant systems. Within the proposed setup, we provide necessary conditions to ensure properties such as controllability, at each time. We show that such model checking controllability properties can be implemented using efficient algorithms (with polynomial complexity). An example, based on the IEEE 5-bus power system, is presented which illustrates our model checking and design methodologies.