The main goal of this thesis was to investigate the use of HA as a unifying systems biology approach to model, simulate and analyze excitable cell networks in general and those of cardiac myocytes in particular. We propose a new biological framework based on the Lynch et al. theory of Hybrid I/O Automata (HIOA) for modeling and simulating excitable tissue. Within this framework, we view an excitable tissue as the composition of two main kinds of components: a diffusion medium and a collection of cells, both modeled as an HIOA. This approach yields a notion of decomposition that allows us to describe a tissue as the parallel composition of several interacting tissues, a property that could be exploited to parallelize, and hence improve, the efficiency of the simulation process. On the basis of HA theory, we have developed CellExcite, an efficient simulation environment for excitable-cell networks. CellExcite allows the user to sketch a tissue of excitable cells, plan the stimuli to be applied during simulation, and customize the diffusion model. CellExcite adopts Hybrid I/O Automata (HIOA) as the computational model in order to efficiently capture both discrete and continuous excitable-cell behavior. We demonstrate the feasibility of our HIOA-based framework to capture and mimic different kinds of wave-propagation behavior in 2D isotropic cardiac tissue, including normal wave propagation along the tissue; the creation of spiral waves; the break-up of spiral waves into more complex patterns such as fibrillation; and the recovery of the tissue to the resting state via electrical defibrillation. We address also the problem of specifying and detecting emergent behavior in networks of cardiac myocytes, spiral electric waves in particular, a precursor to atrial and ventricular fibrillation. To solve this problem we: (1) Apply discrete mode-abstraction to the cycle-linear hybrid automata (CLHA) we have recently developed for modeling the behavior of myocyte networks; (2) Introduce the new concept of spatial-superposition of CLHA modes; (3) Develop a new spatial logic, based on spatial-superposition, for specifying emergent behavior; (4) Devise a new method for learning the formulae of this logic from the spatial patterns under investigation; and (5) Apply bounded model checking to detect (within milliseconds) the onset of spiral waves. We have implemented our methodology as the Emerald tool-suite, a component of our EHA framework for specification, simulation, analysis and control of excitable hybrid automata. We illustrate the effectiveness of our approach by applying Emerald to the scalar electrical fields produced by our CellExcite simulator. Furthermore, we focus our attention on understanding of the synchronized collective behavior that is essential in the networks of pacemaker cells in the heart and could be useful for developing methods to control the dynamics of systems with desired properties. For this purpose we define a subclass of timed automata, called oscillator timed automata, suitable to model biological coupled oscillators. The semantics of their interactions, parametric w.r.t. a model of synchronization, is introduced. We apply it to the Kuramoto model. Then, we introduce a logic, Kuramoto Synchronization Logic (KSL), and a model checking algorithm in order to verify collective synchronization properties of a population of coupled oscillators.
A Formal Framework for Modeling, Simulating and Analyzing Networks of Excitable Cells
BARTOCCI, Ezio
2009-01-15
Abstract
The main goal of this thesis was to investigate the use of HA as a unifying systems biology approach to model, simulate and analyze excitable cell networks in general and those of cardiac myocytes in particular. We propose a new biological framework based on the Lynch et al. theory of Hybrid I/O Automata (HIOA) for modeling and simulating excitable tissue. Within this framework, we view an excitable tissue as the composition of two main kinds of components: a diffusion medium and a collection of cells, both modeled as an HIOA. This approach yields a notion of decomposition that allows us to describe a tissue as the parallel composition of several interacting tissues, a property that could be exploited to parallelize, and hence improve, the efficiency of the simulation process. On the basis of HA theory, we have developed CellExcite, an efficient simulation environment for excitable-cell networks. CellExcite allows the user to sketch a tissue of excitable cells, plan the stimuli to be applied during simulation, and customize the diffusion model. CellExcite adopts Hybrid I/O Automata (HIOA) as the computational model in order to efficiently capture both discrete and continuous excitable-cell behavior. We demonstrate the feasibility of our HIOA-based framework to capture and mimic different kinds of wave-propagation behavior in 2D isotropic cardiac tissue, including normal wave propagation along the tissue; the creation of spiral waves; the break-up of spiral waves into more complex patterns such as fibrillation; and the recovery of the tissue to the resting state via electrical defibrillation. We address also the problem of specifying and detecting emergent behavior in networks of cardiac myocytes, spiral electric waves in particular, a precursor to atrial and ventricular fibrillation. To solve this problem we: (1) Apply discrete mode-abstraction to the cycle-linear hybrid automata (CLHA) we have recently developed for modeling the behavior of myocyte networks; (2) Introduce the new concept of spatial-superposition of CLHA modes; (3) Develop a new spatial logic, based on spatial-superposition, for specifying emergent behavior; (4) Devise a new method for learning the formulae of this logic from the spatial patterns under investigation; and (5) Apply bounded model checking to detect (within milliseconds) the onset of spiral waves. We have implemented our methodology as the Emerald tool-suite, a component of our EHA framework for specification, simulation, analysis and control of excitable hybrid automata. We illustrate the effectiveness of our approach by applying Emerald to the scalar electrical fields produced by our CellExcite simulator. Furthermore, we focus our attention on understanding of the synchronized collective behavior that is essential in the networks of pacemaker cells in the heart and could be useful for developing methods to control the dynamics of systems with desired properties. For this purpose we define a subclass of timed automata, called oscillator timed automata, suitable to model biological coupled oscillators. The semantics of their interactions, parametric w.r.t. a model of synchronization, is introduced. We apply it to the Kuramoto model. Then, we introduce a logic, Kuramoto Synchronization Logic (KSL), and a model checking algorithm in order to verify collective synchronization properties of a population of coupled oscillators.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
