Doi: 10.1145/1467247.1467271
We address 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 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 simulation environment for excitable-cell networks.
One of the most important and intriguing questions in systems biology is how to formally specify emergent behavior in biological tissue, and how to efficiently predict and detect its onset. A prominent example of such behavior is electrical spiral waves in spatial networks of cardiac myocytes (heart cells). Electrical impulses regularly circulate through cardiac tissue and cause the heart’s muscle fibers to contract. In a healthy heart, these electrical impulses travel smoothly and unobstructed, like a water wave that ripples gently in a pond. These waves can, however, sometimes develop into troublesome, whirlpool-like spirals of electrical activity. Spiral waves of this nature are a precursor to a variety of cardiac disturbances, including atrial fibrillation (af), an abnormal rhythm originating in the upper chambers of the heart. af afflicts two–three million Americans alone, putting them at risk for clots and strokes. Moreover, the likelihood of developing af increases with age.
In this paper, we address this question by proposing a simple and efficient method for learning, and automatically detecting the onset of, spiral waves in cardiac tissue. See Figure 1 for an overview of our approach. Underlying our method is a linear spatial-superposition logic (lssl) we have developed for specifying properties of spatial networks. lssl is discussed in greater detail below. Our method also builds upon hybrid automata, image processing, machine learning,
and model-checking techniques to first learn an lssl formula that characterizes such spirals. The formula is then automatically checked against a quadtree representation of the sca-
20
lar electrical field (sef) produced at each discrete time step by a simulation of a hybrid-automata network modeling the myocytes. A scalar field is a function that associates a scalar value, which in our case is an electric potential, to every point in space. The quadtree representation is obtained via discrete mode abstraction and hierarchical superposition of the elementary units within the sef.
The electric behavior of cardiac myocytes is hybrid in nature: they exhibit an all-or-nothing electrical response, the so-called action potential (ap), to an external excitation. An ap can thus be viewed as triggering a discrete mode transition from the cell’s resting mode of continuous behavior to its excited mode of continuous behavior. Despite their discrete-continuous hybrid nature, networks of myocytes have traditionally been modeled using nonlinear partial differential equations. 13, 17 While highly accurate in describing the molecular processes underlying cell behavior—nonlinear differential equations allow one to closely match the values of a multitude of state variables to their actual physical values—these models are not particularly amenable to formal analysis and typically do not scale well for the simulation of complex cell networks.
In Grosu et al., 11 we showed that it is possible to automatically learn a much simpler hybrid automaton (HA) 12 model for cardiac myocytes, which explicitly captures, up to a prescribed error margin, the mixed discrete and continuous behavior of the ap. To highlight its cyclic structure and its linear dynamics, which may vary in interesting ways from cycle to cycle, we called it a cycle-linear hybrid automaton (clha). Moreover, one can use a variant of this clha model to efficiently (up to an order of magnitude faster) and accurately simulate the behavior of myocyte networks, and, in particular, induce spirals and fibrillation. 2, 24, 25
A key observation concerning our simulations, see Figure 3, is that mode abstraction, in which the ap value of each clha in the network is abstracted to its corresponding mode, faithfully preserves the network’s waveform and other spatial characteristics. Hence, for the purpose of learning, and detecting the onset of, spirals within clha networks, we can exploit mode abstraction to dramatically reduce the system state space. A
An earlier version of this paper appeared in Proc. 11th International Conference on Hybrid Systems: Caomputation and Control (HSCC’08), Springer, LNCS 4981, April 2008.
References:
Archives