[Back]


Talks and Poster Presentations (with Proceedings-Entry):

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.



English abstract:
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.


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/2728606.2728609