Supervisor

Suitable for

Abstract

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.