.png){kind=icon}
.png){kind=icon}
Return
Computing compositional proofs of Input-to-Output Stability using SOS optimization and δ-decidability
.png){kind=icon}
PRE
AI
DOI：10.1016/j.nahs.2016.03.008.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
We present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization and delta-decidability over the reals, to compute Bisimulation Functions (BFs) that characterize Input-to-Output Stability (ICS) 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 delta-decidable formula and validated over a level set of the CBF using the dReal tool. If dReal produces a counterexample containing 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. 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 ofBFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current I-Ks 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. (C) 2016 Elsevier Ltd. All rights reserved.
Keywords:
Model-order reduction
Cardiac cell model
Ionic channel
Approximate bisimulation
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
N
IF:
4.1
Papers:
1.4K
Citations:
3.1K
View more organizations