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

We present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization and δ-decidability over the reals, to compute Bisimulation Functions (BFs) that characterize Input-to-Output Stability (IOS) of dynamical systems. BFs are Lyapunov-like functions that decay along the trajectories of a given pair of systems, and can be used to establish the stability of the outputs with respect to bounded input deviations.