an important property when dealing with reactive systems. In our case, it means that we can reason about recursive sqts, i.e., fractals.

The labeling function L defines for each state s ∈ S the set L(s) of atomic formulas that are valid in s. Atomic formulas are inequalities over distributions of the form P[D = m] ∼ d, where D is a distribution function, m ∈ M is a discrete value (e.g. a mode), d ∈ [0.. 1], and ∼ is one of <, ≤, =, ≥, or >. We use P[D = m] as a more intuitive notation for p(m), where p is the pmf associated with D. (This notation is also reminiscent of P[X = m], where X is a random variable.) It should thus be noted that the 0– 1 state labels used in Figure 6, where the mode in question is s, are shorthand for the atomic formula P[D = s] = 0 or P[D = s] = 1.

In order to verify properties of a reactive system modeled as a ks K, it is customary to use either a linear-time or a branching-time temporal logic. A model for a linear-time (ltl) formula is an infinite path p in K. A model for a branching-time formula is K itself; given a state s of K, this allows one to quantify over the paths originating from s. For our current purposes of specifying and detecting the onset of spirals, ltl suffices.

Strictly speaking, our logic is a linear spatial-superposition logic (lssl), as a path p in K represents a sequence of concretizations (anti-superpositions). Syntactically, however, our tem-poral-logic operators are the same as in ltl: the next operator X, with Xj meaning that j holds in a concretization of the current state; its inverse operator B; the until operator U, with j U y meaning that j holds along a path until y holds; and the release operator R, with y Rj meaning that j holds along a path unless released by y.

Definition 4 (lssl Syntax). The syntax of linear spatial- superposition logic is defined inductively as follows:

As discussed above, a bound k on the path length is maintained as a parameter in lssl’s semantic definition.

Definition 5 (lssl Semantics). Let K be a ks, p a path in K, and f ∈ AF an atomic formula. Then, for k ≥ 0, p satisfies an lssl formula j with bound k, written p |= j, only if p |= ⁰j, where:

kk

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

figure 6: Kripke structures for SQGs of figure 5.

x

(a) 1 0 1

1x

10 y

(b)^{0 1 0}

x

(c) ^{1 0}

1x

10 y

(d)

We say that K |= j if for all paths p in K, p |= j.

kk

Our until and release operators U and R are bounded versions of the ltl operators U and R. Similarly, the globally operator G, defined as Gj ≡ ⊥ Rj, is a bounded version of ltl’s G operator. The finally operator F is defined as usual as Fj ≡  Uj. In general, the unbounded ltl version of G is assumed to not hold. For example, Gj does not hold as could be violated at k + 1; to decide Gj in ltl with respect to a bound k, one needs a more sophisticated analysis of the ks K, as discussed in Biere³.

To illustrate lssl, consider a k-unfolding of the ks of Figure 6(a), and assume the distributions labeling the states correspond to mode s. Then, this ks has a path p such that p |=

k

G (P[D = s] = 2/3) holds: the path that always returns to x. To automatically find p, we can model check the negation of this formula; as discussed in Section 5, p will be returned as a counterexample. Using the techniques in Biere³, one can show that p also satisfies the unbounded ltl version of the formula.

5. moDeL checKinG anD LeaRninG

Bounded Model Checking: Given a ks K, lssl formula j, and bound k, a bounded model checker (bmc) efficiently verifies if K |= j . If not, it returns one or more paths p in K that k

violate j (i.e., counterexamples); otherwise, it returns true. Intuitively, a bmc applies the lssl semantics inductively defined in Section 4 to each path p in K. We have implemented a simple prototype bmc for ksss derived from sqts and lssl formulae, which first enumerates all paths in a ks and then for each path applies the lssl semantics. This approach is efficient enough to check within milliseconds the onset of spirals. We are currently improving our handling of safety formulae (those without the F operator) by pruning, during sqt traversal, all subtrees of a vertex as soon as we detect that the current path satisfies j. A more ambitious sat-based bmc is also under development.

Machine learning: Writing the ltl formulae that a reactive system should satisfy is a nontrivial task. Developers often find it difficult to specify system properties of interest. The classification of ltl formulae into safety (something bad should never happen) and liveness properties ( something good should eventually happen) provides some guidance, but the task remains challenging.

Writing lssl formulae describing emerging properties of CLHA networks is even more difficult. For example, what is the lssl formula for spiral onset? In the following, we describe a surprisingly simple, machine-learning-based approach that we have successfully applied to spiral detection. The main idea is to cast the onset property as follows: Is there a path in the given sqt leading to the core of a spiral?,