{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/33802"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/33802","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"Discrete Transition System Model and Verification for Mitochondrially Mediated Apoptotic Signaling Pathways","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Lam, Huy Hong"],"institution":"Virginia Tech","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Electrical and Computer Engineering","degree_department":"Electrical and Computer Engineering","school":null,"contributors":[],"advisors":[],"committee_chairs":["Hsiao, Michael S."],"committee_members":["Abbott, A. Lynn","Samuels, David C."],"year":2007,"date_issued":"2007-06-20","date_published":"2007-06-20","updated_at":"2026-07-22T22:19:13Z","subjects":["SAT","Mitochondria","Model Checking","Reachability Analysis","Generic Algorithm","Apoptosis","Fault Analysis"],"languages":[],"rights":["In Copyright"],"rights_urls":["http://rightsstatements.org/vocab/InC/1.0/"],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["etd-06282007-191549"],"render_values":[{"text":"etd-06282007-191549","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/10919/33802","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeechair","label":"Committee Chair","values":["Hsiao, Michael S."]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Abbott, A. Lynn","Samuels, David C."]},{"key":"dc:contributor.department","label":"Department","values":["Electrical and Computer Engineering"]},{"key":"dc:creator","label":"Author","values":["Lam, Huy Hong"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2014-03-14T20:40:46Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2014-03-14T20:40:46Z","2007-07-13"]},{"key":"dc:date.issued","label":"Date","values":["2007-06-20"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Tech"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical and Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["SAT","Mitochondria","Model Checking","Reachability Analysis","Generic Algorithm","Apoptosis","Fault Analysis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/vocab/InC/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["etd-06282007-191549"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10919/33802"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:title","label":"Title","values":["Discrete Transition System Model and Verification for Mitochondrially Mediated Apoptotic Signaling Pathways"]}]}],"canonical_facts":{"dc:contributor.committeechair":["Hsiao, Michael S."],"dc:contributor.committeemember":["Abbott, A. Lynn","Samuels, David C."],"dc:contributor.department":["Electrical and Computer Engineering"],"dc:creator":["Lam, Huy Hong"],"dc:date.accessioned":["2014-03-14T20:40:46Z"],"dc:date.available":["2014-03-14T20:40:46Z","2007-07-13"],"dc:date.issued":["2007-06-20"],"dc:description.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."],"dc:description.degree":["Master of Science"],"dc:identifier.other":["etd-06282007-191549"],"dc:identifier.uri":["http://hdl.handle.net/10919/33802"],"dc:publisher":["Virginia Tech"],"dc:rights":["In Copyright"],"dc:rights.uri":["http://rightsstatements.org/vocab/InC/1.0/"],"dc:subject":["SAT","Mitochondria","Model Checking","Reachability Analysis","Generic Algorithm","Apoptosis","Fault Analysis"],"dc:title":["Discrete Transition System Model and Verification for Mitochondrially Mediated Apoptotic Signaling Pathways"],"dc:type":["Thesis"],"thesis:degree_discipline":["Electrical and Computer Engineering"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:13Z"}