Computing compositional proofs of Input-to-Output Stability using SOS optimization and δ-decidability

By computing BFs that appeal to a small-gain theorem, the BFComp framework can be used to show that a subsystem of a feedback-composed system can be replaced-with bounded error-by an approximately equivalent abstraction, thereby enabling approximate model-order reduction of dynamical systems. The BFs can then be used to obtain bounds on the error between the outputs of the original system and its reduced approximation. To this end, we illustrate the utility of BFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current IKs can be safely replaced by a one-variable Hodgkin-Huxley-type approximation. In addition to a detailed performance evaluation of BFComp, our case study also presents workarounds for systems with non-polynomial vector fields, which are not amenable to standard SOS optimizers.