Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability.

*(English)*Zbl 1351.93133Summary: 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 (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.

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 of BFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current \(I_{K s}\) 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.

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 of BFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current \(I_{K s}\) 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.

##### MSC:

93D25 | Input-output approaches in control theory |

93B40 | Computational methods in systems theory (MSC2010) |

93C20 | Control/observation systems governed by partial differential equations |

93D30 | Lyapunov and storage functions |

92C50 | Medical applications (general) |

PDF
BibTeX
XML
Cite

\textit{A. Murthy} et al., Nonlinear Anal., Hybrid Syst. 23, 272--286 (2017; Zbl 1351.93133)

Full Text:
DOI

##### References:

[1] | Sontag, E. D., Smooth stabilization implies coprime factorization, IEEE Trans. Automat. Control, 34, 4, (1989) · Zbl 0682.93045 |

[2] | Sontag, E. D., On the input-to-state stability property, Systems Control Lett., 24, 351-359, (1995) · Zbl 0877.93121 |

[3] | Sontag, E. D., Input to state stability: basic concepts and results, (Nonlinear and Optimal Control Theory, (2006), Springer), 163-220 · Zbl 1175.93001 |

[4] | Liberzon, D., Switching in systems and control, (2003), Springer · Zbl 1036.93001 |

[5] | Jiang, Z. P.; Mareels, I. M.Y.; Wang, Y., A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica, 32, 8, 1211-1215, (1996) · Zbl 0857.93089 |

[6] | A. Girard, G.J. Pappas, Approximate bisimulations for nonlinear dynamical systems, in: Proceedings of 44th IEEE Conference on Decision and Control, Serville, Spain, December 2005. |

[7] | Girard, A.; Pappas, G. J., Approximate bisimulation relations for constrained linear systems, Automatica, 43, 8, 1307-1317, (2007) · Zbl 1130.93365 |

[8] | Girard, A.; Pappas, G. J., Approximation metrics for discrete and continuous systems, IEEE Trans. Automat. Control, 52, 5, 782-798, (2007) · Zbl 1366.93032 |

[9] | A. Girard, A composition theorem for bisimulation functions. Pre-print, 2007. arXiv:1304.5153. |

[10] | A.A. Julius, G.J. Pappas, Approximate equivalence and approximate synchronization of metric transition systems, in: Proceedings of 45th IEEE Conference on Decision and Control, San Diego, CA, 2006, December 2006. |

[11] | Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008 |

[12] | Islam, M. A.; Murthy, A.; Girard, A.; Smolka, S. A.; Grosu, R., Compositionality results for cardiac cell dynamics, (Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, (2014), ACM) · Zbl 1362.92017 |

[13] | Girard, A.; Pappas, G. J., Hierarchical control system design using approximate simulation, Automatica, 45, 2, 566-571, (2009) · Zbl 1158.93301 |

[14] | Rungger, Matthias; Zamani, Majid, Compositional construction of approximate abstractions, (Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (2015), ACM), 68-77 · Zbl 1364.93286 |

[15] | J. Lygeros, G. Pappas, S. Sastry, An introduction to hybrid systems modeling, analysis and control, in: Preprints of the First Nonlinear Control Network Pedagogical School, 1999, pp. 307-329. |

[16] | Huang, Z.; Fan, C.; Mereacre, A.; Mitra, S.; Kwiatkowska, M., Invariant verification of nonlinear hybrid automata networks of cardiac cells, (Proceedings of 26th International Conference on Computer Aided Verification (CAV), LNCS, vol. 8559, (2014), Springer), 373-390 |

[17] | Duggirala, P. S.; Mitra, S.; Viswanathan, M., Verification of annotated models from executions, (Proceedings of the Eleventh ACM International Conference on Embedded Software, EMSOFT ’13, (2013), IEEE Press Piscataway, NJ, USA), 26:1-26:10 |

[18] | Gao, S.; Kong, S.; Clarke, E. M., Dreal: an SMT solver for nonlinear theories over the reals, (Automated Deduction-CADE-24, (2013), Springer), 208-214 · Zbl 1381.68268 |

[19] | S. Prajna, A. Papachristodoulou, P. Seiler, P.A. Parrilo, SOSTOOLS: Sum of squares optimization toolbox for MATLAB, 2004. |

[20] | Iyer, V.; Mazhari, R.; Winslow, R. L., A computational model of the human left-ventricular epicardial myocytes, Biophys. J., 87, 3, 1507-1525, (2004) |

[21] | M.A. Islam, A. Murthy, Supplementary document, 2014. URL: www.cs.sunysb.edu/ amurthy/hscc15_supp.htm. |

[22] | Murthy, Abhishek; Ariful Islam, Md.; Smolka, Scott A.; Grosu, Radu, Computing bisimulation functions using SOS optimization and \(\delta\)-decidability over the reals, (Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (2015), ACM), 78-87 · Zbl 1364.93728 |

[23] | Murthy, A.; Islam, M. A.; Bartocci, E.; Cherry, E.; Fenton, F. H.; Glimm, J.; Smolka, S. A.; Grosu, R., Approximate bisimulations for sodium channel dynamics, (Proceedings of CMSB’12, the 10th Conference on Computational Methods in Systems Biology, LNCS, (2012), Springer London, UK) |

[24] | Islam, M. A.; Murthy, A.; Bartocci, E.; Cherry, E. M.; Fenton, F. H.; Glimm, J.; Smolka, S. A.; Grosu, R., Model-order reduction of ion channel dynamics using approximate bisimulation, Theoret. Comput. Sci., (2014) |

[25] | Islam, Md. A.; Murthy, A.; Bartocci, E.; Smolka, S. A.; Grosu, R., Compositionality results for cardiac cell dynamics, (Proceedings of CMSB’13, the 11th Conference on Computational Methods in Systems Biology, LNCS, (2013), Springer Klosterneuburg, Austria) |

[26] | Prajna, S.; Jadbabaie, A., Safety verification of hybrid systems using barrier certificates, (Hybrid Systems: Computation and Control, (2004), Springer), 477-492 · Zbl 1135.93317 |

[27] | Gao, S.; Avigad, J.; Clarke, E. M., Delta-complete decision procedures for satisfiability over the reals, (Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR’12, (2012), Springer-Verlag Berlin, Heidelberg), 286-300 · Zbl 1358.03028 |

[28] | Gao, S.; Avigad, J.; Clarke, E. M., Delta-decidability over the reals, (Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS), 2012, (2012), IEEE), 305-314 · Zbl 1364.03065 |

[29] | MATLAB Open curve fitting toolbox (cftool). Version 7.10.0 (R2010a). The MathWorks Inc., Natick, Massachusetts, 2010. |

[30] | Jeffreys, H.; Jeffreys, B., Methods of mathematical physics, (2000), Cambridge Mathematical Library · Zbl 0037.31704 |

[31] | Bauer, F. L.; Fike, C. T., Norms and exclusion theorems, Numer. Math., (1960) · Zbl 0101.25503 |

[32] | Gao, S.; Avigad, J.; Clarke, E. M., \(\delta\) completee decision procedures for satisfiability over the reals, (Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR’12, (2012), Springer-Verlag Berlin, Heidelberg), 286-300 · Zbl 1358.03028 |

[33] | J. Kapinski, A. Donzé, F. Lerda, H. Maka, S. Wagner, B.H. Krogh, Control software model checking using bisimulation functions for nonlinear systems, in: 47th IEEE Conference on Decision and Control (CDC), 2008, pp. 4024-4029. |

[34] | Prajna, S.; Jadbabaie, A.; Pappas, G. J., A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Trans. Automat. Control, 52, 8, 1415-1429, (2007) · Zbl 1366.93711 |

[35] | V.A. Yakubovich, G.A. Leonov, A.K. Gelig, Stationary sets in control systems with discontinuous nonlinearities (series on stability, vibration and control of systems, series a, 14), 2004. · Zbl 1054.93002 |

[36] | Kapinski, J.; Deshmukh, J. V.; Sankaranarayanan, S.; Arechiga, N., Simulation-guided Lyapunov analysis for hybrid dynamical systems, (Hybrid Systems: Computation and Control (HSCC), (2014), ACM Press), 133-142 · Zbl 1362.93108 |

[37] | Sassi, M. A.B.; Sankaranarayanan, S.; Chen, X.; Abraham, E., Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis, IMA J. Math. Control Inform., (2015) |

[38] | S. Sankaranarayanan, X. Chen, E. Abraham, Lyapunov function synthesis using Handelman representations, in: IFAC conference on Nonlinear Control Systems (NOLCOS), 2013, pp. 576-581. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.