---
_id: '4527'
abstract:
- lang: eng
text: |-
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 gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the 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.
acknowledgement: Supported in part by the Swiss National Science Foundation (grant
205321-111840).
alternative_title:
- LNCS
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. Bounded asynchrony: Concurrency
for modeling cell-cell interactions. In: Vol 5054. Springer; 2008:17-32. doi:10.1007/978-3-540-68413-8_2'
apa: 'Fisher, J., Henzinger, T. A., Mateescu, M., & Piterman, N. (2008). Bounded
asynchrony: Concurrency for modeling cell-cell interactions (Vol. 5054, pp. 17–32).
Presented at the FMSB: Formal Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-540-68413-8_2'
chicago: 'Fisher, Jasmin, Thomas A Henzinger, Maria Mateescu, and Nir Piterman.
“Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions,” 5054:17–32.
Springer, 2008. https://doi.org/10.1007/978-3-540-68413-8_2.'
ieee: 'J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman, “Bounded asynchrony:
Concurrency for modeling cell-cell interactions,” presented at the FMSB: Formal
Methods in Systems Biology, 2008, vol. 5054, pp. 17–32.'
ista: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. 2008. Bounded asynchrony:
Concurrency for modeling cell-cell interactions. FMSB: Formal Methods in Systems
Biology, LNCS, vol. 5054, 17–32.'
mla: 'Fisher, Jasmin, et al. Bounded Asynchrony: Concurrency for Modeling Cell-Cell
Interactions. Vol. 5054, Springer, 2008, pp. 17–32, doi:10.1007/978-3-540-68413-8_2.'
short: J. Fisher, T.A. Henzinger, M. Mateescu, N. Piterman, in:, Springer, 2008,
pp. 17–32.
conference:
name: 'FMSB: Formal Methods in Systems Biology'
date_created: 2018-12-11T12:09:19Z
date_published: 2008-05-26T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '26'
doi: 10.1007/978-3-540-68413-8_2
extern: 1
intvolume: ' 5054'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf
month: '05'
page: 17 - 32
publication_status: published
publisher: Springer
publist_id: '196'
quality_controlled: 0
status: public
title: 'Bounded asynchrony: Concurrency for modeling cell-cell interactions'
type: conference
volume: 5054
year: '2008'
...