Probabilistic model checking for cellular microcolonies
The gro language enables the programming, modelling, specifying and visually simulating the behaviour of cells in growing
microcolonies of microorganisms (http://depts.washington.edu/soslab/gro/index.html). 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 (www.prismmodelchecker.org) 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.