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

生物系统模型包括多个随机的、通常是多尺度的、在不同时间尺度上执行的生物过程，例如分子过程与细胞过程的通信。形式化的方法，如模型检测，已被用作了解生物过程通信细节的查询机制。在生物过程的系统级建模中，实验数据的不精确性和不完备性要求构建新的理论框架和形式化分析算法。该项目结合不确定条件下生物学中多尺度随机模型的构建，及时、恰当地解决了模型检验中的状态爆炸问题。构造用于多尺度随机系统模型检测的新的模型降阶算法对于严格评估用时态逻辑表示的查询是至关重要的。该项目的目标是为随机系统的多尺度模型的形式化分析建立一个坚实的理论框架，并为不确定条件下生物过程的有效查询机制开发创新的模型。在该项目中开发的工具将是开源的。这项研究的跨学科性质将为本科生提供机会，让他们在计算机科学、数学、化学和生物学之间进行思想的交流。拟议工作的影响将推动在不确定条件下对大系统进行严格的形式化分析和系统生物学建模的极限。该项目的目标是：i)发展描述不确定随机系统中多尺度过程的理论形式化，以便进行形式化分析；ii)创建和评估有效的算法来查询不确定随机系统模型。建立和评估不确定条件下的随机模型。当与实验数据相结合时，新的框架将提供简洁和精确的生物过程模型。该项目将在一个以本科生为主的机构(PUI)进行。该项目的教材将用于不同级别的本科课程。该项目将以培养跨学科研究人员为目标，通过本科生班级的重点小型课程项目提供研究经验。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.