Type
Text
Type
Dissertation
Advisor
Grosu, Radu | Tannenbaum, Allen | Fenton, Flavio. | Smolka, Scott A
Date
2014-12-01
Keywords
Computer science | Bisimulation Functions, Computational Modeling, Feedback Compositionality, Input-to-State Stability, Model-Order Reduction, Towers of Abstraction
Department
Department of Computer Science.
Language
en_US
Source
This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree.
Identifier
http://hdl.handle.net/11401/77301
Publisher
The Graduate School, Stony Brook University: Stony Brook, NY.
Format
application/pdf
Abstract
Modeling, analysis, and control of cardiac excitation, the biological process cardiac cells undergo on a periodic basis, is indispensable for understanding and countering life-threatening electrical disturbances of the heart, such as atrial and ventricular fibrillation. Modeling involves the derivation of a mathematical/computational representation of the dynamics of cardiac cells and their diffusivity. The key to effective modeling lies in striking a balance between i) precision, the ability of the model to replicate the underlying biological phenomena, and ii) performance, in terms of amenability to automated analysis techniques, such as simulation and formal verification. The techniques of abstraction and compositionality have been instrumental in striking this balance. Abstraction is the process of removing unnecessary detail from a given model so that the resulting abstract version is both observationally equivalent to the original model and a conservative approximation of it, but better suited for the analysis of the properties of interest. Given a system consisting of a number of interacting components, also known as subsystems, Compositionality enables us to substitute a component by its equivalent abstraction, such that the overall system retains the properties of interest. In the case of real-valued continuous-time dynamical systems, such as cardiac-cell models, a notion of approximate equivalence has been proposed, which can be used to show that an abstraction is approximately equivalent to the concrete model. Care must be taken, however, when a concrete model of a system component C is replaced by an approximately equivalent abstraction C' within a feedback loop; in such situations, the approximation error between C and C' may get amplified. For feedback compositions, Antoine Girard has shown that Lyapunov-like Bisimulation Functions (BFs) satisfying a certain Small Gain Theorem can be used to establish substitutivity, which follows from i) input-to-state stability of the concrete and abstract subsystems, and ii) the robustness of the rest of the system to input deviations. In this thesis, we first extend BFs to handle input-to-output stability and present two Sum-of-Squares formulations for automating the search for BFs. The automated proof technique, which has been implemented using MATLAB SOSTOOLS, enables component-wise approximate model-order reduction of feedback-composed dynamical systems. Using our techniques, we show that within a detailed 67-variable cardiac-cell model, the 13- and 10-variable Markovian subsystems for sodium and potassium channels can be safely (with bounded error) substituted by two-variable Hodgkin-Huxley-type models. The two-variable abstractions were identified using using a two-step curve fitting technique. We then present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for computing the curvature of electrical waves and their associated breakup in cardiac tissues. Given a digitized frame of a propagating wave, SCA constructs a highly accurate representation of the front and the back of the wave, piecewise interpolates this representation with cubic splines, and subjects the result to an accurate curvature analysis. SCA has been applied to a number of representative types of spiral waves, and, for each type, a distinct curvature evolution in time (signature) has been identified. Finally, we present explicit and online Model-Predictive Controllers for an excitable-cell simulator based on the nonlinear FitzHugh-Nagumo model. Despite the plant's nonlinearity, we formulate the control problem as an instance of quadratic programming, using a piecewise affine abstraction of the plant. The speed-versus-accuracy tradeoff for the explicit and online versions is analyzed on various reference trajectories. | 125 pages
Recommended Citation
Murthy, Abhishek, "Computational Modeling and Analysis of Cardiac Excitation" (2014). Stony Brook Theses and Dissertations Collection, 2006-2020 (closed to submissions). 3122.
https://commons.library.stonybrook.edu/stony-brook-theses-and-dissertations-collection/3122