--- _id: '2302' abstract: - lang: eng text: 'We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only "significant" mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model''s variables.' author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Maria full_name: Mateescu, Maria id: 3B43276C-F248-11E8-B48F-1D18A9856A87 last_name: Mateescu citation: ama: Henzinger TA, Mateescu M. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 2012;10(2):310-322. doi:10.1109/TCBB.2012.91 apa: Henzinger, T. A., & Mateescu, M. (2012). The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE. https://doi.org/10.1109/TCBB.2012.91 chicago: Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE, 2012. https://doi.org/10.1109/TCBB.2012.91. ieee: T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical reaction networks,” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2. IEEE, pp. 310–322, 2012. ista: Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 10(2), 310–322. mla: Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:10.1109/TCBB.2012.91. short: T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322. date_created: 2018-12-11T11:56:52Z date_published: 2012-07-03T00:00:00Z date_updated: 2021-01-12T06:56:38Z day: '03' department: - _id: ToHe - _id: CaGu doi: 10.1109/TCBB.2012.91 ec_funded: 1 external_id: pmid: - '22778152' intvolume: ' 10' issue: '2' language: - iso: eng month: '07' oa_version: None page: 310 - 322 pmid: 1 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: IEEE ACM Transactions on Computational Biology and Bioinformatics publication_status: published publisher: IEEE publist_id: '4625' quality_controlled: '1' scopus_import: 1 status: public title: The propagation approach for computing biochemical reaction networks type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 10 year: '2012' ... --- _id: '3136' abstract: - lang: eng text: 'Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event''s initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag.' acknowledgement: This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation. alternative_title: - LNCS author: - first_name: Calin C full_name: Guet, Calin C id: 47F8433E-F248-11E8-B48F-1D18A9856A87 last_name: Guet orcid: 0000-0001-6220-2052 - first_name: Ashutosh full_name: Gupta, Ashutosh id: 335E5684-F248-11E8-B48F-1D18A9856A87 last_name: Gupta - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Maria full_name: Mateescu, Maria id: 3B43276C-F248-11E8-B48F-1D18A9856A87 last_name: Mateescu - first_name: Ali full_name: Sezgin, Ali id: 4C7638DA-F248-11E8-B48F-1D18A9856A87 last_name: Sezgin citation: ama: 'Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309. doi:10.1007/978-3-642-31424-7_24' apa: 'Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., & Sezgin, A. (2012). Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358, pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_24' chicago: Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,” 7358:294–309. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_24. ieee: 'C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed continuous time Markov chains for genetic regulatory circuits,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.' ista: 'Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification, LNCS, vol. 7358, 294–309.' mla: Guet, Calin C., et al. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits. Vol. 7358, Springer, 2012, pp. 294–309, doi:10.1007/978-3-642-31424-7_24. short: C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer, 2012, pp. 294–309. conference: end_date: 2012-07-13 location: Berkeley, CA, USA name: 'CAV: Computer Aided Verification' start_date: 2012-07-07 date_created: 2018-12-11T12:01:36Z date_published: 2012-07-01T00:00:00Z date_updated: 2021-01-12T07:41:18Z day: '01' department: - _id: CaGu - _id: ToHe doi: 10.1007/978-3-642-31424-7_24 ec_funded: 1 language: - iso: eng month: '07' oa_version: None page: 294 - 309 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '3561' quality_controlled: '1' scopus_import: 1 status: public title: Delayed continuous time Markov chains for genetic regulatory circuits type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: '7358 ' year: '2012' ... --- _id: '3834' abstract: - lang: eng text: "Background\r\n\r\nThe chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species.\r\nResults\r\n\r\nIn order to show the effectiveness of our approach, we apply it to several examples previously described in the literature. The experimental results show that the proposed method speeds up the analysis considerably, compared to a global analysis, while still providing high accuracy.\r\n\r\n\r\nConclusions\r\n\r\nThe sliding window method is a novel approach to address the performance problems of numerical algorithms for the solution of the chemical master equation. The method efficiently approximates the probability distributions at the time points of interest for a variety of chemically reacting systems, including systems for which no upper bound on the population sizes of the chemical species is known a priori." acknowledgement: This research has been partially funded by the Swiss National Science Foundation under grant 205321-111840 and by the Cluster of Excellence on Multimodal Computing and Interaction at Saarland University. author: - first_name: Verena full_name: Wolf, Verena last_name: Wolf - first_name: Rushil full_name: Goel, Rushil last_name: Goel - first_name: Maria full_name: Mateescu, Maria id: 3B43276C-F248-11E8-B48F-1D18A9856A87 last_name: Mateescu - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Wolf V, Goel R, Mateescu M, Henzinger TA. Solving the chemical master equation using sliding windows. BMC Systems Biology. 2010;4(42):1-19. doi:10.1186/1752-0509-4-42 apa: Wolf, V., Goel, R., Mateescu, M., & Henzinger, T. A. (2010). Solving the chemical master equation using sliding windows. BMC Systems Biology. BioMed Central. https://doi.org/10.1186/1752-0509-4-42 chicago: Wolf, Verena, Rushil Goel, Maria Mateescu, and Thomas A Henzinger. “Solving the Chemical Master Equation Using Sliding Windows.” BMC Systems Biology. BioMed Central, 2010. https://doi.org/10.1186/1752-0509-4-42. ieee: V. Wolf, R. Goel, M. Mateescu, and T. A. Henzinger, “Solving the chemical master equation using sliding windows,” BMC Systems Biology, vol. 4, no. 42. BioMed Central, pp. 1–19, 2010. ista: Wolf V, Goel R, Mateescu M, Henzinger TA. 2010. Solving the chemical master equation using sliding windows. BMC Systems Biology. 4(42), 1–19. mla: Wolf, Verena, et al. “Solving the Chemical Master Equation Using Sliding Windows.” BMC Systems Biology, vol. 4, no. 42, BioMed Central, 2010, pp. 1–19, doi:10.1186/1752-0509-4-42. short: V. Wolf, R. Goel, M. Mateescu, T.A. Henzinger, BMC Systems Biology 4 (2010) 1–19. date_created: 2018-12-11T12:05:25Z date_published: 2010-04-08T00:00:00Z date_updated: 2021-01-12T07:52:32Z day: '08' ddc: - '005' department: - _id: ToHe doi: 10.1186/1752-0509-4-42 file: - access_level: open_access checksum: 220239fae76f7b03c4d7f05d74ef426f content_type: application/pdf creator: system date_created: 2018-12-12T10:16:29Z date_updated: 2020-07-14T12:46:16Z file_id: '5217' file_name: IST-2012-72-v1+1_Solving_the_chemical_master_equation_using_sliding_windows.pdf file_size: 1919130 relation: main_file file_date_updated: 2020-07-14T12:46:16Z has_accepted_license: '1' intvolume: ' 4' issue: '42' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 1 - 19 publication: BMC Systems Biology publication_status: published publisher: BioMed Central publist_id: '2374' pubrep_id: '72' quality_controlled: '1' scopus_import: 1 status: public title: Solving the chemical master equation using sliding windows tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 4 year: '2010' ... --- _id: '3843' abstract: - lang: eng text: "Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous- time Markov chain (CTMC).\r\nStandard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process.\r\nIn this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks." acknowledgement: This research has been partially funded by the Swiss National Science Foundation under grant 205321-111840 and by the Cluster of Excellence on Multimodal Computing and Interaction at Saarland University. article_processing_charge: No author: - first_name: Frédéric full_name: Didier, Frédéric last_name: Didier - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Maria full_name: Mateescu, Maria id: 3B43276C-F248-11E8-B48F-1D18A9856A87 last_name: Mateescu - first_name: Verena full_name: Wolf, Verena last_name: Wolf citation: ama: 'Didier F, Henzinger TA, Mateescu M, Wolf V. Fast adaptive uniformization of the chemical master equation. In: Vol 4. IEEE; 2009:118-127. doi:10.1109/HiBi.2009.23' apa: 'Didier, F., Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Fast adaptive uniformization of the chemical master equation (Vol. 4, pp. 118–127). Presented at the HIBI: High-Performance Computational Systems Biology, Trento, Italy: IEEE. https://doi.org/10.1109/HiBi.2009.23' chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf. “Fast Adaptive Uniformization of the Chemical Master Equation,” 4:118–27. IEEE, 2009. https://doi.org/10.1109/HiBi.2009.23. ieee: 'F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Fast adaptive uniformization of the chemical master equation,” presented at the HIBI: High-Performance Computational Systems Biology, Trento, Italy, 2009, vol. 4, no. 6, pp. 118–127.' ista: 'Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Fast adaptive uniformization of the chemical master equation. HIBI: High-Performance Computational Systems Biology vol. 4, 118–127.' mla: Didier, Frédéric, et al. Fast Adaptive Uniformization of the Chemical Master Equation. Vol. 4, no. 6, IEEE, 2009, pp. 118–27, doi:10.1109/HiBi.2009.23. short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, IEEE, 2009, pp. 118–127. conference: end_date: 2009-10-16 location: Trento, Italy name: 'HIBI: High-Performance Computational Systems Biology' start_date: 2009-10-14 date_created: 2018-12-11T12:05:28Z date_published: 2009-10-30T00:00:00Z date_updated: 2023-02-23T11:45:05Z day: '30' ddc: - '000' department: - _id: ToHe - _id: CaGu doi: 10.1109/HiBi.2009.23 file: - access_level: open_access checksum: 9a3bde48f43203991a0b3c6a277c2f5b content_type: application/pdf creator: dernst date_created: 2020-05-19T16:33:55Z date_updated: 2020-07-14T12:46:17Z file_id: '7874' file_name: 2009_HIBI_Didier.pdf file_size: 222890 relation: main_file file_date_updated: 2020-07-14T12:46:17Z has_accepted_license: '1' intvolume: ' 4' issue: '6' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 118 - 127 publication_status: published publisher: IEEE publist_id: '2348' quality_controlled: '1' related_material: record: - id: '3842' relation: later_version status: public scopus_import: 1 status: public title: Fast adaptive uniformization of the chemical master equation type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 4 year: '2009' ... --- _id: '4453' abstract: - lang: eng text: We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology. acknowledgement: The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840. alternative_title: - LNCS author: - 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: Verena full_name: Wolf, Verena last_name: Wolf citation: ama: 'Henzinger TA, Mateescu M, Wolf V. Sliding-window abstraction for infinite Markov chains. In: Vol 5643. Springer; 2009:337-352. doi:10.1007/978-3-642-02658-4_27' apa: 'Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Sliding-window abstraction for infinite Markov chains (Vol. 5643, pp. 337–352). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_27' chicago: Henzinger, Thomas A, Maria Mateescu, and Verena Wolf. “Sliding-Window Abstraction for Infinite Markov Chains,” 5643:337–52. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_27. ieee: 'T. A. Henzinger, M. Mateescu, and V. Wolf, “Sliding-window abstraction for infinite Markov chains,” presented at the CAV: Computer Aided Verification, 2009, vol. 5643, pp. 337–352.' ista: 'Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352.' mla: Henzinger, Thomas A., et al. Sliding-Window Abstraction for Infinite Markov Chains. Vol. 5643, Springer, 2009, pp. 337–52, doi:10.1007/978-3-642-02658-4_27. short: T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:55Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:57:04Z day: '01' doi: 10.1007/978-3-642-02658-4_27 extern: 1 file: - access_level: open_access checksum: 36b974111521ea534aae294166e93a63 content_type: application/pdf creator: system date_created: 2018-12-12T10:12:20Z date_updated: 2020-07-14T12:46:30Z file_id: '4938' file_name: IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf file_size: 804295 relation: main_file file_date_updated: 2020-07-14T12:46:30Z intvolume: ' 5643' main_file_link: - open_access: '0' url: http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf month: '01' oa: 1 page: 337 - 352 publication_status: published publisher: Springer publist_id: '278' pubrep_id: '40' quality_controlled: 0 status: public title: Sliding-window abstraction for infinite Markov chains type: conference volume: 5643 year: '2009' ... --- _id: '4535' abstract: - lang: eng text: |- Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required. acknowledgement: This research was supported in part by the Swiss National Science Foundation under grant 205321-111840 and by the Excellence Cluster on Multimodal Computing and Interaction. alternative_title: - LNCS author: - first_name: Frédéric full_name: Didier, Frédéric last_name: Didier - 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: Verena full_name: Wolf, Verena last_name: Wolf citation: ama: 'Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities in noisy cellular processes. In: Vol 5688. Springer; 2009:173-188. doi:10.1007/978-3-642-03845-7_12' apa: 'Didier, F., Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Approximation of event probabilities in noisy cellular processes (Vol. 5688, pp. 173–188). Presented at the CMSB: Computational Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-642-03845-7_12' chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf. “Approximation of Event Probabilities in Noisy Cellular Processes,” 5688:173–88. Springer, 2009. https://doi.org/10.1007/978-3-642-03845-7_12. ieee: 'F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event probabilities in noisy cellular processes,” presented at the CMSB: Computational Methods in Systems Biology, 2009, vol. 5688, pp. 173–188.' ista: 'Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Approximation of event probabilities in noisy cellular processes. CMSB: Computational Methods in Systems Biology, LNCS, vol. 5688, 173–188.' mla: Didier, Frédéric, et al. Approximation of Event Probabilities in Noisy Cellular Processes. Vol. 5688, Springer, 2009, pp. 173–88, doi:10.1007/978-3-642-03845-7_12. short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 173–188. conference: name: 'CMSB: Computational Methods in Systems Biology' date_created: 2018-12-11T12:09:21Z date_published: 2009-08-17T00:00:00Z date_updated: 2023-02-23T11:24:03Z day: '17' doi: 10.1007/978-3-642-03845-7_12 extern: 1 intvolume: ' 5688' month: '08' page: 173 - 188 publication_status: published publisher: Springer publist_id: '189' quality_controlled: 0 related_material: record: - id: '3364' relation: later_version status: public status: public title: Approximation of event probabilities in noisy cellular processes type: conference volume: 5688 year: '2009' ... --- _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' ...