propagation. The first set of images was used to train the
classifier; we supervised the training by discriminating
between paths leading to a spiral core versus those (of maximum pmf) belonging to images that did not contain a spiral. From this first set we extracted 512 possible paths, and
used Weka to build a ruled-based classifier with a very high
prediction accuracy ( 99.25%).
The test set was divided into increasingly larger sets
of images: 500, 550, 600, and 650 images. Applying the
rule-based classifier on the first 500 images produced 67
wrongly classified paths. We used these paths to obtain a
new, retrained classifier. We then used both classifiers on
the remaining sets of images, and for each classifier and
test set we computed the lssl formula accuracy, as an estimate of how well the formula specifies the spatial pattern.
As Table 1 shows, retraining considerably improves accuracy, and can be repeated each time a false classification
Weka’s decision-tree algorithm took less than 9s to
construct a rule-based classifier from the training (512
records) and retraining (579 records) tables, respectively.
Our model checker took between 1. 67 and 7.09s, with an
average of 4.72s to model check the sqt for a 400 × 400 sef
if no spiral was present, and between 1 ms and 4.64s, with
an average of 230ms otherwise. All results were obtained
on a PC equipped with a Centrino 2GHz processor with
figure 7: EMERALD bounded model checker.
104 communications of the acm | march 2009 | Vol. 52 | no. 3
7. ReLateD WoRK
The use of hybrid automata to model and analyze spatial
networks is a relatively new subject area, and includes
application to Delta-Notch signaling networks, 9
coordinated control of autonomous underwater vehicles, 19 and
aircraft trajectories and landing protocols. 7, 21 In contrast,
our focus is on emergent behavior (in the form of spiral
waves) in networks of cardiac myocytes, and the use of spatial superposition as an abstraction mechanism. Predicting
spirals4 in pure continuous models23 is a more complicated
process than what is implemented in Emerald, where discrete sqt structures, obtained via mode abstraction and
superposition, are used. Several logics have recently been
proposed for describing the behavior and spatial structure of concurrent systems, 5, 6 and for reasoning about the
topological aspects of modal logics and Kripke structures. 1
Unlike lssl, these logics are not based on an abstraction
mechanism like spatial-superposition that can be used to
alleviate state explosion during model checking.
In this paper, we have presented a framework for specifying and detecting emergent behavior in networks of cardiac myocytes. Our approach, which uses hybrid automata,
discrete mode abstraction, and bounded model checking,
is based on a novel notion of spatial superposition and its
related logic LSSL, and a new method for the automated
learning of formulae in this logic from the spatial patterns under investigation. Our framework has been fully
implemented in the Emerald tool suite. Our preliminary
experimental results are very encouraging, with a prediction accuracy of over 93% on a test set comprising 650
images. As future work, we plan to extend our framework
to the learning of branching-time spatial-superposition
properties and the more intricate problem of specifying
and detecting spatiotemporal emergent behavior.
We also experimented with the SIFT (Scale-Invariant
Feature Transform) algorithm, which detects and matches
interesting features in images while preserving invari-ance constraints for scaling, translation, and rotation.
We found that SIFT performed matching well on images
of spirals that were related to one another through rigid
transformations. It was less successful, due to an insufficient number of matching keypoints, on spirals with more
markedly different shapes. Also, SIFT and other image-processing techniques tend to process the entire image. Our
approach, in contrast, uses logical formulae over sqt paths
and densities of a particular clha mode (stimulated) along
table 1: experimental results.
Path classifier test set
Trained (512 paths)
Retrained (512 paths + 67