As biomedical research advances into more complicated systems, there is an increasing need to model and analyze these systems to better understand them. Formal specification and analyzing methods, such as model checking techniques, hold great promise in helping further discovery and innovation for complicated biochemical systems. Models can be tested and adapted inexpensively in-silico providing new insights. However, development of accurate and efficient modeling methodologies and analysis techniques are still open challenges for biochemical systems. This thesis is focused on designing appropriate modeling formalisms and efficient analyzing algorithms for various biological systems in three different thrusts:

• Modeling Formalisms: we have designed a multi-scale hybrid rule-based modeling formalism to depict intra- and intercellular dynamics using discrete and continuous variables respectively. Its hybrid characteristic inherits advantages of logic and kinetic modeling approaches.

• Formal Analyzing Algorithms: 1) We have developed a LTL model checking algorithm for Qualitative Networks (QNs). It considers the unique feature of QNs and combines it with over-approximation to compute decreasing sequences of reachability set, resulting in a more scalable method. 2) We have developed a formal analyzing method to handle probabilistic bounded reachability problems for two kinds of stochastic hybrid systems considering uncertainty parameters and probabilistic jumps. It combines a SMT-based model checking technique with statistical tests in a sound manner. Compared to standard simulation-based methods, it supports non-deterministic branching, increases the coverage of simulation, and avoids the zero-crossing problem. 3) We have designed a new framework, where formal methods and machine learning techniques take joint efforts to enhance the understanding of biological and biomedical systems. Within this framework, statistical model checking is used as a (sub)model selection method.

• Applications: To check the feasibility of our model language and algorithms, wehave 1) constructed Boolean Network models for the signaling network for single pancreatic cancer cell, and used symbolical model checking to analyze these models, 2) built Qualitative Network models describing cellular interactions during skin cells' differentiation, and applied our improved bounded LTL model checking technique, 3) developed a multi-scale hybrid rule-based model for the pancreatic cancer micro-environment, and employed statistical model checking, 4) created a nonlinear hybrid model to depict a bacteria-killing process, and adopted a recently promoted δ-complete decision procedure-based model checking technique, 5) extended hybrid models for atrial fibrillation, prostate cancer treatment, and our bacteria-killing process into stochastic hybrid models, and applied our probabilistic bounded reachability analyzer SReach, and 6) carried out the probabilistic reachability analysis of the tap withdrawal circuit in C. elegans using SReach.

149 pages

Thesis Committee:
Edmund M. Clarke (Chair)
Stephen Brookes
Frank Pfenning
Marta Zofia Kwiakowska (University of Oxford)
Natasa Miskov-Zivanov (University of Pittsburgh)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science