Celiku_Friedenberg_2022 -- Probabilistic Model Checking of Cancer Metabolism

We provide a model of glycolysis and TCA cycle in cancers in which IDH is encountered both in its wild type form as well as mutated and capable of catalyzing an onco-metabolite. The model is constructed using the Probabilistic Symbolic Model Checker (PRISM,https://www.prismmodelchecker.org/) specification language, and properties are specified using a temporal-property specification language. The reaction rates are instantiated using both experimentally derived metabolic flux rate data (under normoxia and hypoxia conditions) as well as derived through a combination of these experimental rates and relative enzyme activity levels estimated using mRNA expression data from patient samples. We provide shell scripts for invoking the freely-available automatic model checker for reasoning about the specified properties.