A Logical Framework for Modelling Breast Cancer Progression

Data streams for a personalised breast cancer programme could include collections of image data, tumour genome sequencing, likely at the single cell level, and liquid biopsies (DNA and Circulating Tumour Cells (CTCs)). Although they are rich in information, the full power of these datasets will not be realised until we develop methods to model the cancer systems and conduct analyses that transect these streams. In addition to machine learning approaches, we believe that logical reasoning has the potential to provide help in clinical decision support systems for doctors. We develop a logical approach to modelling cancer progression, focusing on mutation analysis and CTCs, which include the appearance of driver mutations, the transformation of normal cells to cancer cells in the breast, their circulation in the blood, and their path to the bone. Our long term goal is to improve the prediction of survival of metastatic breast cancer patients. We model the behaviour of the CTCs as a transition system, and we use Linear Logic (LL) to reason about our model. We consider several important properties about CTCs and prove them in LL. In addition, we formalise our results in the Coq Proof Assistant, thus providing formal proofs of our model. We believe that our results provide a promising proof-of-principle and can be generalised to other cancer types and groups of driver mutations.