| dcterms.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. <italic>Abstraction</italic> 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, <italic>Compositionality</italic> 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 <italic>Bisimulation Functions </italic>(BFs) satisfying a certain Small Gain Theorem can be used to establish substitutivity, which follows from i) <italic>input-to-state stability</italic> of the concrete and abstract subsystems, and ii) the <italic>robustness</italic> of the rest of the system to input deviations. In this thesis, we first extend BFs to handle <italic>input-to-output stability</italic> and present two <italic>Sum-of-Squares formulations</italic> for automating the search for BFs. The automated proof technique, which has been implemented using MATLAB SOSTOOLS, enables <italic>component-wise approximate model-order reduction of feedback-composed dynamical systems</italic>. 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 <italic>Spiral Classification Algorithm<italic> (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 <italic>Model-Predictive Controllers</italic> 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. | |
