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
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.
for further details.
The code was tested in Coq 8.7.2. The main files are:
- Library LL:
Specification of linear logic (syntax, rules and basic proof theory)
- Library BioLL: Definition of biological rules, automation techniques and proofs of properties of interest
The files can be downloaded here
The full list of files (and documentation) is here
For further information, please contact Carlos Olarte
Joëlle Despeyroux, Amy Felty, Pietro Lio and Carlos Olarte: A Logical Framework for Modelling Breast Cancer Progression
Submitted to MLCSB'18. (PDF).
Is it possible for a CTC, with mutations EPCAM,CD47
and fitness 3
to become an extravasating CTC with fitness 8
? What is the
time delay for such transition ?
What is the time delay for a CTC with mutations EPCAM, CD47
and fitness 3
to become an extravasating CTC with fitness between 6
A cell in the breast, with mutation EP
, might have his fitness oscillating from 1
and back ?
We prove some properties that require reasoning on the meta-level
(e.g., checking whether it is possible to fire a rule or not and then,
showing the resulting state).
Any cell having a null fitness must go to apoptosis
The following property states one of the key properties of our model: Any
cell in the blood has four possible evolutions:
- acquiring passenger mutations: its fitness decreases by one and the driver
mutations remain unchanged;
- going to apoptosis;
- acquiring a driver mutation: its fitness increases by two;
- moving to the bone: its fitness increases by one and the driver mutations EPCAM, CD47, CD44, MET remain unchanged.