where the core of a spiral is the central point from which the spiral emanates, getting progressively farther away as it revolves around the point.

The implementation of our approach is simple as well. For an sef (a 400×400 array of ap values) produced by the CellExcite simulator (see Figure 1), our Emerald tool set allows the user to select a path through the sef’s corresponding sqt simply by clicking on a point in the sef, e.g. in the core of a spiral. If no spiral is present, the sqt path with maximum pmf (probability mass function) is returned. Note that this method is not restricted to spirals: path selection via clicking on a representative point can be applied to normal wave propagation, wave collision, etc.

The paths so obtained are then used to learn the lssl formula for the property in question, such as spiral onset. The learning algorithm works as follows: ( 1) For each path of length k, where k is the height of the sqt, we define k attributes a ,…, a such that each a holds the pmf value of vertex

1k i v , for the mode we are interested in (for spirals, mode s). ( 2) i

Each path is classified by Emerald as spiral or nonspiral depending on whether or not the user clicked on a point (core); the classification is stored as an additional classifier attribute c. ( 3) All records (a ,…, a , c) are stored in a table,

ik

which is provided to the data-classification phase. ( 4) At the end of this phase, we obtain a path classifier which we translate into an lssl formula.

Data classification²² is generally a two-step process: training and testing. For training, we choose a classification algorithm that learns a set of descriptions of our training data set. The form of these descriptions depends on the type of classification algorithm employed. For testing, we use a test data set, disjoint from the training set and containing the class attribute with a known value. The accuracy of the classifier on a given test set is the percentage of the test records that are correctly classified. Various techniques can be used to obtain test and training sets from an initial set of records, such as X-Cross Validation. ⁸

For classification purposes, we use a descriptive classifier (dc), which returns a set of if–then rules called discriminant rules. Underlying dcs are decision trees, rough sets, classification-by-association analysis, etc. A rule r has the form

where I is a subset of [ 1..k]. Usually, each class c has an associated set of rules r , …, r ; i.e., c is characterized by ⁿ r .

1 n i= 1 i

Using boolean arithmetic, this is equivalent to

The antecedent formula ⁿ  a = v is called the class- i= 1 j∈I ij ij

i description formula of the class c.

As is customary, we built a classifier for one class only (the class c), called the target class, using all other classes as one contrasting class. Hence the classifier consists of only one class-description formula, describing the target class. We say that we learned that formula. We have used Weka’s

decision-tree algorithm, but any other rule-based algorithm could have been used as well. The classifier we have learned for spirals is as follows:

if a <= 0.875 then

7

if a <= 0.048 then ∼c else c
2
else if a3 <= 0.078 then
if a0 <= 0.025 then ∼c else c
else ∼c

Its translation into lssl, where x^k stands for k repetitions of x, generated the following formula:

X² P(D = s)>0.048 ∧ X⁷ P(D = s)≤0.875 Ú

P(D = s)>0.025 ∧ X³ P(D = s)≤0.078 ∧ X⁷ P(D = s)>0.875

This formula is an approximate description of a spiral which we use together with Emerald’s bmc to detect spiral onset within milliseconds. In case the bmc returned a false positive, we add the corresponding record to the classification table as part of a retraining phase; see Figure 1.

6. imPLementation

Our techniques of Sections 2–5 have been implemented as the Emerald tool suite of the eha environment. Emerald is a Java application that can be used to learn an lssl formula for a particular spatial pattern, and to check the formula against a set of images (of the kind pictured on the right-hand side of Figure 3) that reproduce the discrete behavior of a clha network. For ease of use, Emerald provides two graphical tools, one for Preprocessing ( classification) and the other for Bounded Model Checking.

The Preprocessing tool enables users to browse the various collections of images they have assembled for machine-learning purposes, and to view their sqt representation. The user can select a path leading to a spiral core by clicking on an appropriate stimulated point (in yellow) of the image. If the image does not contain a spiral, the user can choose the maximum pmf path or a generic stimulated point. Each path selected is stored in a data table in the form of the pmf sequence of stimulated modes in each node of the traversed sqt. All such paths are subsequently exported to Weka in a common format. Presently, we have customized Emerald for spiral detection, but we plan to extend the tool with the capability to classify any generic spatial pattern.

The bmc applet (Figure 7) enables the user to check an lssl formula against the sqt representation of a specific image. As discussed in Section 5, the lssl formula encodes the classifier for the spatial pattern under investigation. If the sqt in question fails to satisfy the formula, the resulting counterexamples (spirals) are reported to the user both as rows in the counterexample table and as red dots marking the core of the spiral contained in the image.

Table 1 contains our preliminary experimental results. For training and testing purposes, we used two different sets of images, each containing spirals and normal wave