Tag Archives: model checking


SyncMore travel for me and another great book.  This one is Sync: How Order Emerges from Chaos in The Universe, Nature, and Daily Live by Steven Strogatz.

The simplest example,  echoed on the book cover, is how do millions of fireflies synchronize their blinking.  There is no global “blink now” clock.  There is no master firefly orchestrating the performance.  So how do the fireflies end up synchronized?  It’s a simple idea that requires a lot of thought to truly understand.  The problem seems so simple when you first hear it.  I would have probably waved my hands at it, mumbled that the solution probably looked like XYZ, and then moved on. Only when you really try to solve it, do you begin to see the depth and subtly of this particular rat hole.

Strogatz also discusses many other sync problems:  pairs of electrons in superconductors, pacemaker cells in the heart, hints at neurons in the brain, and many others.  I was particularly intrigued by his discussion of the propagation of chemical activation waves in 2 and 3 dimensions.

There are no equations in the book, but Strogatz’s prose is sufficient to give a good taste of the novel mathematics he and others have used to address these problems.  It was a quick read.

As with most books I read, I begin to ponder how I might apply some of its ideas to multiagent systems.  For one, there are multiple ties to social networking (the A is-connected-to B kind; not the Twitter kind).  I also try to re-imagine his waves of chemical activations around a Petri dish transformed into waves of protocol interactions around a social network.

Most of Strogatz’s problems appear to require continuous-space and continuous-time.  Most of my multiagent system problems are simpler, requiring only discrete-space and discrete-time. I’ve developed some “half-vast” (say it out loud) ideas about using a model checker to approach protocol problems with sync-like elements.  I’d introduce some social operators into the model and an expanded CTL-like expression language.  Models would only need to be expanded enough to check the specific properties under consideration.  I’d also need to introduce agent variables that range over a group of agents to express the kinds of properties I have in mind.  The classic CTL temporal operators are strictly time-like, whereas the social operators would be strictly space-like.  Unfortunately, my current ideas could easily cause a massive state space explosion, so I still have work to do.

I so love reading books like Sync:  books that open intellectual doors and expand conceptual horizons.  I expect I’ll be thinking about these ideas for quite some time.