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 |= 0j, 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 Biere3.
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 Biere3, 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?,