EAGER: Formal Analysis of Stochastic Models in Systems Biology Under Uncertainty

生物系统模型由多个随机的、通常是多尺度的、在不同时间尺度上执行的生物过程组成，例如分子过程与细胞过程的通信。正式的方法，如模型检查，已被用作查询机制，以了解生物过程的通信细节。生物过程系统级建模中实验数据的不精确性和不完整性要求建立新的理论框架和形式化分析算法。该项目在解决不确定条件下生物多尺度随机模型构建与模型验算中的状态爆炸问题方面具有较强的应用性。构建用于多尺度和随机系统模型检查的新型模型约简算法对于严格评估以时间逻辑表示的查询至关重要。该项目的目标是为随机系统的多尺度模型的形式化分析建立一个坚实的理论框架，并为不确定性下生物过程的有效查询机制开发创新模型。项目中开发的工具将是开源的。该研究的跨学科性质将为本科生提供计算机科学、数学、化学和生物学之间思想交流的机会。所提出的工作的影响将推动在不确定性下对大型系统进行严格形式分析和系统生物学建模的极限。本项目的目标是：i)发展不确定性下随机系统中多尺度过程的理论形式，用于形式分析；ii)创建和评估不确定性下随机系统模型查询的有效算法。不确定性下的随机模型的模型将被创建和评估。当与实验数据相结合时，新的框架将提供简洁和精确的生物过程模型。该项目将在一所本科院校（PUI）进行。该项目的教材将用于不同层次的本科课程。该项目将通过专注于本科生的迷你课程项目提供研究经验，目标是培养跨学科研究人员。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Biological system models comprise of multiple biological processes that are stochastic and often, multiscale, processes executing at different time scales such as communication of molecular processes with cellular processes. Formal methods such as model checking have been used as a querying mechanism to understand the details of communication of biological processes. The imprecision and incompleteness of experimental data in system level modeling of biological processes necessitates construction of novel theoretical framework and algorithms for formal analysis. The project is timely and appropriate in addressing the challenges of the state explosion problem in model checking combined with construction of multiscale and stochastic models in biology under uncertainty. The construction of novel model reduction algorithms for model checking of multiscale and stochastic systems becomes essential for a rigorous evaluation of queries represented in temporal logic. The goal of this project is to create a solid theoretical framework for formal analysis of multiscale models of stochastic systems and develop innovative models for efficient querying mechanisms for biological processes under uncertainty. Tools developed in the project will be open-sourced. The interdisciplinary nature of the research will provide opportunities for undergraduates for cross-fertilization of ideas between computer science, mathematics, chemistry and biology.The impact of proposed work will push the limits in modeling a large system under uncertainty for rigorous formal analysis and modeling in systems biology. The goal of this project is pursued by the aims, i) Develop theoretical formalism representing multiscale processes in stochastic systems under uncertainty for formal analysis and ii) Create and evaluate efficient algorithms for querying on models of stochastic systems under uncertainty. Models of stochastic models under uncertainty will be created and evaluated. The novel framework will provide succinct and precise models of biological processes when combined with experimental data. The project will be conducted at a primarily undergraduate institution (PUI). Educational materials from the project will be used at different levels of undergraduate curriculum. The project will provide research experiences through focused mini-course projects in undergraduate classes with the goal of developing interdisciplinary researchers.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.