Type of Document	Master's Thesis
Author	Lam, Huy Hong
Author's Email Address	lamhuy@vt.edu
URN	etd-06282007-191549
Title	Discrete Transition System Model and Verification for Mitochondrially Mediated Apoptotic Signaling Pathways
Degree	Master of Science
Department	Electrical and Computer Engineering
Advisory Committee	Advisor Name Title Dr. Michael S. Hsiao Committee Chair Dr. A. Lynn Abbott Committee Member Dr. David C. Samuels Committee Member
Keywords	SAT Mitochondria Model Checking Reachability Analysis Generic Algorithm Apoptosis Fault Analysis
Date of Defense	2007-06-20
Availability	unrestricted
Abstract Computational biology and bioinformatics for apoptosis have been gaining much momentum due to the advances in computational sciences. Both fields use extensive computational techniques and modeling to mimic real world behaviors. One problem of particular interest is on the study of reachability, in which the goal is to determine if a target state or protein concentration in the model is realizable for a signaling pathway. Another interesting problem is to examine faulty pathways and how a fault can make a previously unrealizable state possible, or vice versa. Such analysis can be extremely valuable to the understanding of apoptosis. However, these analyses can be costly or even impractical for some approaches, since they must simulate every aspect of the model. Our approach introduces an abstracted model to represent a portion of the apoptosis signaling pathways as a finite state machine. This abstraction allows us to apply hardware testing and verification techniques and also study the behaviors of the system without full simulation. We proposed a framework that is tailor-built to implement these verification techniques for the discrete model. Through solving Boolean constraint satisfaction problems (SAT-based) and with guided stimulation (Genetic Algorithm), we can further extract the properties and behaviors of the system. Furthermore, our model allows us to conduct cause-effect analysis of the apoptosis signaling pathways. By constructing single- and double-fault models, we are able to study what fault(s) can cause the model to malfunction and the reasons behind it. Unlike simulation, our abstraction approach allows us to study the system properties and system manipulations from a different perspective without fully relying on simulation. Using these observations as hypotheses, we aim to conduct laboratory experiments and further refine our model.
Files	Filename       Size       Approximate Download Time (Hours:Minutes:Seconds)     28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access    huylam_msthesis_revised.pdf 611.14 Kb 00:02:49 00:01:27 00:01:16 00:00:38 00:00:03

If you have questions or technical problems, please Contact DLA.