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 is returned.

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 1.5GB RAM.

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, ⁹ coordinated control of autonomous underwater vehicles, ¹⁹ 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 spirals⁴ in pure continuous models²³ 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. ¹ 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.

8. concLusion

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.

15

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 such paths.

table 1: experimental results.

Path classifier test set

(550) 87.00% 97.10%

Trained (512 paths) Retrained (512 paths + 67 counterexamples)

test set
(600)
88.83%
97.33%

test set
(650)
88.23%
93.07%