Formal analysis for logical models of pancreatic cancer

We apply formal verification techniques for studying the behavior of signaling pathways important in cancer. In particular, we use Model Checking for verifying behavioral properties of a single-cell, in silico model of pancreatic cancer. We are interested in properties associated with apoptosis (programmed cell death), cell cycle arrest and proliferation. The properties are specified in temporal logics and include, for example, whether there are checkpoints that the cancer cell should go through before it reaches a given state. Our model includes several major signaling pathways, including the Hedgehog, WNT, KRAS, RB-E2F, NFkB, p53, TGFβ, and apoptosis pathways, which have been recently found to be mutated frequently in pancreatic cancer. The model is formally analyzed via symbolic Model Checking, and shown to agree well qualitatively with experiments. We conclude that Model Checking offers a powerful approach for studying logical models of relevant biological processes.