A Logical Framework for Modelling Breast Tumorigenosis


General Information

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. See [DFLO18] for further details.

Download

The code was tested in Coq 8.7.2. The main files are: The files can be downloaded here. The full list of files (and documentation) is here. For further information, please contact Carlos Olarte.

References

[DFLO18] Joëlle Despeyroux, Amy Felty, Pietro Lio and Carlos Olarte: A Logical Framework for Modelling Breast Cancer Progression Submitted to MLCSB'18. (PDF).

Reachability Properties

Property 1
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 ?

Lemma Property1: ∀ n t,
 |-F- Theory ; [ E{ fun _ x ⇒ perp (TX{ var x} )} ** (C{ n; bone; 8; EPCDCDME} ⁻) ;
 Atom T{ Cte t} ; Atom C{ n ; blood ; 3 ; EPCD}] ; UP [] .
Property 2
What is the time delay for a CTC with mutations EPCAM, CD47 and fitness 3 or 4 to become an extravasating CTC with fitness between 6 and 9 ?
Lemma Property2: ∀ n t,
 |-F- Theory ; [E{ fun _ x ⇒ perp (TX{ var x} )} ** ( (C{ n ; bone ; 6 ; EPCDCDME} ⁻)
  ⊕ (C{n ; bone ; 7 ; EPCDCDME}⁻) ⊕ (C{n ; bone ; 8 ; EPCDCDME}⁻ )
  ⊕ (C{n ; bone ; 9 ; EPCDCDME}⁻) )] ;
    UP [T{ Cte t} ⁺ ; C{ n ; blood ; 3 ; EPCD}⁺ & C{ n ; blood ; 4 ; EPCD}⁺ ] .
Property 3
A cell in the breast, with mutation EP , might have his fitness oscillating from 1 to 2 and back ?
Lemma Property3_Seq1: ∀ n t,
    ∃ d,  |-F- Theory ; [ E{ fun _ x ⇒ perp TX{ fc1 d (var x)}} ** (C{ n; breast; 2; EP} ⁻) ;
 Atom T{ Cte t} ; Atom C{ n ; breast ; 1 ; EP}] ; UP [] .

Lemma Property3_Seq2: ∀ n t,     ∃ d,
 |-F- Theory ; [ E{ fun _ x ⇒ perp TX{ fc1 d (var x)}} ** (C{ n; breast; 1; EP} ⁻) ;
 Atom T{ Cte t} ; Atom C{ n ; breast ; 2 ; EP}] ; UP [] .

Meta-level Properties

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).
Property 4
Any cell having a null fitness must go to apoptosis
Proposition Property4 :
  ∀ (n t :nat) c lm ,
  |-F- Theory ; [ Atom T{ Cte t} ; Atom C{ n ; c; 0 ; lm} ] ; UP [] →
  ∃ d, |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom A{ n } ] ; UP [].
Property 5
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.
Definition GoalP5 (f n t m:nat) :=
 |-F- Theory ; [ Atom T{ Cte t} ; Atom C{ n ; blood; f ; m} ] ; UP [] →
 ∃ (d m' :nat),
  |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;blood; f -1; m } ] ; UP [] ∨
  |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom A{ n} ] ; UP [] ∨
  (|-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;blood; f +2; m' } ] ; UP [] ∧ (plusOne m m') ) ∨
  (m = EPCDCDME ∧ |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;bone; f + 1; EPCDCDME } ] ; UP []) .
Proposition Property5 : ∀ (f n t m:nat) ,
    GoalP4 f n t m.