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
v , for the mode we are interested in (for spirals, mode s). ( 2)
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,
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 classification22 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. 8
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
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 n r .
1 n i= 1 i
Using boolean arithmetic, this is equivalent to
The antecedent formula n a = v is called the class-
i= 1 j∈I ij ij
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
if a <= 0.048 then ∼c else c
else if a3 <= 0.078 then
if a0 <= 0.025 then ∼c else c
Its translation into lssl, where xk stands for k repetitions
of x, generated the following formula:
X2 P(D = s)>0.048 ∧ X7 P(D = s)≤0.875 Ú
P(D = s)>0.025 ∧ X3 P(D = s)≤0.078 ∧ X7 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.
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