A. Murthy, A. Islam, S. Smolka, R. Grosu:

"Computing Bisimulation Functions using SOS Optimisation and delta-decidability over the Reals";

Talk: 18th International Conference on Hybrid Systems: Computation and Control (HSCC), Seattle, USA; 2015-04-13 - 2015-04-15; in: "HSCC 2015", ACM, (2015), ISBN: 978-1-4503-3433-4; 78 - 87.

hscc15.bsf

by Grosu Radu - last modified Jun 11, 2015 11:45 AM - History

Murthy/Islam/Smolka/Grosu

Computing Bisimulation Functions using SOS

Optimization and Î´-Decidability over the Reals.*

A. Murthy, A. Islam, S.A. Smolka, and R. Grosu

We present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization

and Î´-decidability over the reals to compute Bisimulation Functions (BFs) that char- acterize

input-to-output stability 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. In addition to establishing IOS,

BFComp is designed to provide tight bounds on the squared output errors between systems

whenever possible. For this purpose, two SOS optimization formulations are employed: SOSP

1, which enforces the decay requirements on a discretized grid over the input space, and

SOSP 2, which covers the input space exhaustively. SOSP 2 is attempted first, and if the

resulting error bounds are not satisfactory, SOSP 1 is used to compute a Candidate BF (CBF).

The decay requirement for the BFs is then encoded as a Î´-decidable formula and validated

over a level set of the CBF using the dReal tool. If dReal produces a counterexample

comprising the states and inputs where the decay requirement is violated, this pair of vectors

is used to refine the input-space grid and SOSP 1 is iterated. 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. We illustrate the utility of BFComp on a canonical cardiac-cell model,

showing that 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 Proc. of HSCC'15, the 18th International Conference on Hybrid Systems: Computation and

Control, Seattle, USA, April, 2015. ACM Press.

*This work was partially supported by the NSF-Expeditions CMACS Award CNS-09-26190,

FWF-NFN RiSE Award, FWF-DC LMCS Award, FFG Harmonia Award, and FFG Em2Apps

Award.

http://dx.doi.org/10.1145/2728606.2728609

Created from the Publication Database of the Vienna University of Technology.