Communications - March 2009

in 2D isotropic (homogeneous) cardiac tissue, including normal wave propagation (1–150ms); the creation of spirals, a precursor to fibrillation (200–250ms); and the break-up of such spirals into more complex spatiotemporal patterns, signaling the transition to vf (250–400 ms).

As can be clearly seen in Figure 3, mode abstraction, in which the action-potential value of each clha in the network is discretely abstracted to its corresponding mode, faithfully preserves the network’s waveform and other spatial characteristics. Hence, for the purpose of learning and detecting spirals within clha networks, we can exploit mode abstraction to dramatically reduce the system state space.

3. suPeRPosition anD QuaDtRees

A key benefit of using hybrid automata compared to nonlinear odes is their explicit support for finitary abstractions: the infinite range of values of a hybrid automaton’s continuous state variables can be abstracted to the automaton’s discrete finite set of modes. As discussed in Sections 1 and 2, abstracting the ap (voltage) of the constituent clha in a clha network to

figure 3: simulation of continuous and discrete behavior of a CLHA network.

Continuous behavior

mV

− 80− 66− 52− 38− 24− 10 4 18 32 46 60

Discrete behavior
Resting Plateau
Stimulated Upstroke

1 ms

1� Stimulus

50 ms

100 ms

Normal wave propagation

150 ms

200 ms

250 ms

300 ms

350 ms

400 ms

2� Stimulus

Ventricular fibrillation

100 communications of the acm | march 2009 | Vol. 52 | no. 3

their corresponding mode (s, u, p, or r) turns out to faithfully preserve the network’s waveform and other spatial characteristics. This simplifying approximation allows us to reduce the spiral-onset verification problem to a finite-state verification problem.

Although in this paper we consider a clha network an execution at a time, our ultimate goal is exhaustive simulation, i.e., model checking. Within this context, the state space of a 400 × 400 clha network, which would be necessary to simulate the behavior of a tissue of about 16 cm² in size, is still too large for analysis purposes: it has 4^160,000 mode values! To combat state explosion, we use a spatial abstraction inspired by Kwon and Agha. ¹⁴ Consider the state space of a clha network. We regard the current mode of each clha in the network as a degenerate probability distribution, and define the superposition of a set of (possibly superposed) modes as the mean of their distributions. By successively applying superposition to the clha network, we obtain a tree whose root is the mode superposition of the entire network, and whose leaves are the individual modes of the component clha. The particular superposition tree structure we employ, the quadtree, was inspired by image-processing techniques. ²⁰

Let A be a 2^k × 2^k matrix of clha modes. A quadtree Q = (V, R) representation of A is a quaternary tree, such that each vertex v ∈ V represents a sub-matrix of A and the transition relation R defines v ’s 4 child vertices (assuming v is not a leaf ). For example, the root v of the quadtree in Figure 4 represents

0

the entire matrix; child v represents the matrix {2^k^{− 1}, …, 2^k} ×

1

{0,…, 2^k^{− 1}}; child v represents the matrix {2^k^{− 1}, …, 3 2^k^{− 2}} ×

6

{0, …, 2^k^{− 2}}; etc.

Due to superposition, a quadtree is in general a more efficient data structure than the matrix it represents: if the subtree rooted at a node of a quadtree is of one “color” (mode in our case), then there is no need to descend into the node’s subtree as no additional information can be gleaned by doing so. Moreover, given a quadtree representation of an image and a property of the image in which one is interested—such as determining whether a mode-abstracted snapshot of a clha network contains a spiral—it may only be necessary to follow a path through the quadtree (as opposed to exploring the entire tree) to determine if the property holds. Moreover, the path need not necessarily descend all the way to the leaf level, but rather may terminate at an interior node. See Sections 4 and 5 for a further discussion of such quadtree properties.

Definition 1 (Distributions). Let N be a clha network whose constituent clha have (ordered) modes M = {s, u, p,

r}, and let Q be the quadtree representation of N. Then each
leaf node l ∈ Q has an associated degenerate leaf distribution
D whose probability mass function (also sometimes known
l
as the point mass function, and in either case abbreviated