Skip to main content

Probabilistic model checking for cellular microcolonies


Suitable for


The gro language enables the programming, modelling, specifying and visually simulating the behaviour of cells in growing microcolonies of microorganisms ( gro has been used for teaching of synthetic biology. Microcolonies develop through e.g. cell division and cell growth, and can be described in a simple guarded command language. This project aims to extend the gro framework with probabilistic model checking by translating the language to the PRISM modelling language ( and extending the functionality to allow for model checking queries specified in probabilistic temporal logic. The project would suit a student interested in programming and synthetic biology.