Predicting Protein Folding Kinetics Via Temporal Logic Model Checking

Christopher James Langmead⋆ and Sumit Kumar Jha Department of Computer Science, Carnegie Mellon University We present a novel approach for predicting protein folding kinetics using techniques from the field of model checking. This represents the first time model checking has been applied to a problem in the field of structural biology. The protein’s energy landscape is encoded symbolically using Binary Decision Diagrams and related data structures. Questions regarding the kinetics of folding are encoded as formulas in the temporal logic CTL. Model checking algorithms are then used to make quantitative predictions about the kinetics of folding. We show that our approach scales to state spaces as large as 1023 when using exact algorithms for model checking. This is at least 14 orders of magnitude larger than the number of configurations considered by comparable techniques. Furthermore, our approach scales to state spaces at least as large as 1032 unique configurations when usin...

• Type: Conference
• Year: 2007
• Where: WABI
• Authors: Christopher James Langmead, Sumit Kumar Jha
• Keywords: Algorithms, Model Checking, Model Checking Algorithms, Protein Folding Kinetics, WABI 2007