## Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions

*Jasmin Fisher,
Thomas A. Henzinger,
Maria Mateescu, and Nir Piterman*

We introduce *bounded asynchrony*, a notion of concurrency
tailored to the modeling of biological cell-cell interactions.
Bounded asynchrony is the result of a scheduler that bounds the number
of steps that one process can get ahead of other processes; this allows
the components of a system to move independently while keeping them
coupled. Bounded asynchrony accurately reproduces some experimental
observations made about certain cell-cell interactions: its
constrained nondeterminism captures the variability observed in cells
that, although equally potent, assume distinct fates. Real-life cells
are not "scheduled," but we show that distributed real-time behavior
can lead to component interactions that are observationally equivalent
to bounded asynchrony; this provides a possible mechanistic
explanation for the phenomena observed during cell fate specification.

We use model checking to determine cell fates. The nondeterminism of
bounded asynchrony causes state explosion during model checking, but
partial-order methods are not directly applicable. We present a new
algorithm that reduces the number of states that need to be explored:
our optimization takes advantage of the bounded-asynchronous progress
and the spatially local interactions of components that model cells.
We compare our own communication-based reduction with partial-order
reduction (on a restricted form of bounded asynchrony), and experiments
illustrate that our algorithm leads to significant savings.

*Proceedings of the
First International Workshop on Formal Methods in Systems Biology*
(FMSB),
Lecture Notes in Computer Science 5054,
Springer,
2008,
pp. 17-32.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 Springer.