Formal Methods for Biological Systems: Languages, Algorithms, and Applications
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2016
- Accession Number
- AD1025787
Entities
People
- Qinsi Wang
Organizations
- Carnegie Mellon University