The project originates from the combined efforts of researchers from different fields such as model checking, logics, process algebras, network science, constraints, hybrid systems. The goal is to extend and refine methods and software modules for modeling, analysis and synthesis of complex systems involving many, possibly partially known components which interact at different levels, involving also parameters and stochastic effects. Such interactions can produce dramatic effects and methods for the systematic analysis of the expected behaviors are necessary together with techniques for the synthesis of controllers/plans ensuring safety.

We are motivated by two observations: crucial aspects of such systems cannot be properly captured exploiting only one of the current existing approaches; recent advances in different formalisms make them mature for integration. We rely on a set of existing tools: temporal networks, process algebras, and automata as modeling languages; temporal logics, metric interval temporal logics, logic of knowledge, non-monotonic logics, logical frameworks, and behavioral equivalences as querying formalisms; constraint solvers and GPU implementations as efficient engines.

Instead of developing a general framework we focus on the analysis of two case studies: the European Train Control System (ETCS) and Breast Cancer Progression (BCP). On ETCS we will cooperate with FBK working on it since 2008. In BCP the models have to be inferred from existing descriptions and clinical data (see, e.g., cBioPortal data on detailed type Invasive Breast Carcinoma).

The novelty and effectiveness of our proposal is a consequence of the following peculiarities. The team members have complementary expertises and they have already cooperated on publications, tools, and projects. The efforts will be focused on the two selected case studies.

Reviews and general introductions

  1. The evolution of tumour phylogenetics: principles and practice: an interesting view on the state-of-art of tumour phylogenetics methods, a really good introduction to this field
  2. Computational Cancer Biology: An Evolutionary Perspective: brief introduction on general methods used for cancer phylogenetics
  3. An Introduction to Hidden Markov Models and Bayesian Network: tutorial on the theoretical aspects of various HMM and BN variants


  1. Create Markov Chains from different types of cancer data (ENCASE tool)
  2. Inferring Cancer Progression from Single-cell Sequencing while Allowing Mutation Losses: generation of phylogeny trees using Dollo-k (a mutation in a gene can be lost and reacquired k times)
  3. LOBICO: tool to generate drug response models (article)
  4. TRONCO: set of many different tools for cancer phylogenetic
  5. CAPRI: part of TRONCO, specifically made for cross-sectional data
  6. TRaIT: part of TRONCO, specifically made for single cell and bulk analysis
  7. BML (Bayesian Mutation Landscape): tool that reconstruct mutation (SNV only) progression using bayesan networks , an improved version can be found here with also a general guide (in italian)

Markov Models

  1. Stochastic State Transitions Give Rise to Phenotypic Equilibrium in Populations of Cancer Cells: use of Markov Chains to describe proportions of cell types in breast cancer
  2. New Probabilistic Network Models and Algorithms for Oncogenesis: 2006 work using Hidden Markov Models to model the evolution of chromosomical level modifications
  3. A Hidden Markov Model for Cancer Progression: usage of HMMs learned with maximum likelihood estimates to model aberrations progression


  1. Intra-tumour diversification in colorectal cancer at the single-cell level: study on few patients using single cell analysis revealing that the desease evolution was quite different for each tumor (this work was described by Carla Piazza in one of our meetings)


  1. GDSC (Genomics of Drug Sensitivity in Cancer): Information on effects of drugs on cancer (see also this article)
  2. COSMIC (Catalogue Of Somatic Mutations In Cancer): association of recurring mutations in cancer and their effects
  3. cBio portal data sets: collection of the majority of the publicated dataset on tumors, they are mainly made of cross-sectional data
  4. TGCA (The Cancer Genome Atlas)
  5. ICGC (International Cancer Genome Consortium)
  6. FireBrowse: alternative to cBio portal
  7. PharmgKB: informations on drugs
  8. Pathway Commons: visualization of pathways informations

Reading list