Computer Science Thesis Proposal

Thursday, March 31, 2016 - 10:00am


Traffic 21 Classroom 6501 Gates & Hillman Centers


QINSI WANG, Ph.D. Student

For More Information, Contact:

Formal methods hold great promise in promoting further discovery and innovation for complicated biological systems. Models can be tested and adapted inexpensively in-silico to provide new insights. However, development of accurate and efficient modeling methodologies and analysis techniques is still an open challenge. This thesis proposal 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 (MSHR) 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. Compared to standard simulation-based methods, it supports non-deterministic branching, increases the coverage of simulation, and avoids the zero-crossing problem. 3) We are designing a new framework, where formal methods and machine learning techniques take joint efforts to automate the model design of biological systems. Within this framework, model checking can also be used as a (sub)model selection method. 4) We will propose a model checking technique for general stochastic hybrid systems (GSHSs) where, besides probabilistic transitions, stochastic differential equations are used to capture continuous dynamics. Applications: To check the feasibility of our modeling language and algorithms, we have constructed and studied 1) Boolean network models of the signaling network within pancreatic cancer cells, 2) QN models describing cellular interactions during skin cells' differentiation, 3) a MSHR model of the pancreatic cancer micro-environment, 4) a hybrid automaton of our light-aided bacteria-killing process, 5) extended stochastic hybrid models for atrial fibrillation, prostate cancer treatment, and our bacteria-killing process, and 6) a GSHS model depicting population changes of different species within the algae-fish-bird freshwater ecosystem considering distinct doses of estrogen injected. Thesis Committee:Edmund M. Clarke (Chair)Stephen BrookesFrank PfenningJasmin Fisher (University of Cambridge and Microsoft Research)Marta Zofia Kwiatkowska (University of Oxford) Copy of Proposal Document


Thesis Proposal