Process Algebra Approaches to Collective Dynamics

The aim of this scientific research programme is to help to understand how we can predict the dynamic behaviour of a population when we can model the behaviour of the individuals.There are application areas in many scientific fields for a question such as this, but one of the most important is in biology. Biologists study cells, reagents, molecules, and molecular complexes in order to gain insights into growth and change. Here carefully defined models have increasing importance because more and more biological research is now being done using computer-based analysis. That form of research complements the biological research which is traditional laboratory science, based on controlled experiments, data gathering, and observation. Models allow the biologists to try to make sense of the data they have observed, forming hypotheses which may then be tested in further experiments. Their research findings inspire the design of new drugs and treatments which fight illness and improve human and animal health.Scientists need languages in order to communicate effectively and unambiguously. The models developed by biologists are often written in the mathematical notation for calculus invented by Leibniz, as differential equations. Whilst this notation has many virtues it is not always the most intuitive to use, and can be far removed from the cellular processes being described. So biologists have been investigating the use of other system description languages, from other areas of science.Computer science has more experience than the other sciences in formal language design. In computer science formal languages have been used for a variety of purposes, one of which is the design and validation of programs. One class of languages which have been used for this purpose are process algebras, which as well as features for describing systems, come equipped with techniques for comparing systems and proving properties about them. Formal languages such as process algebras do not evolve naturally in the way that human languages do. Instead, they need to be carefully designed.This fellowship will bring the benefits of the experience of computer science in formal language design to the design of a new process algebra for modelling biological systems, the language BioSPA. One crucial aspect of this new language will be its use of mathematically quantified randomness. In every living thing is a controlled amount of randomness because living things are fuelled by chemical reactions. Systems of chemical reactions evolve stochastically because of the inherent randomness of thermal molecular motion.The BioSPA language will be supported by software tools which will allow biologists to see their models in a number of ways. For example, as a Markov process, a mathematical process which randomly moves between a number of distinct states, or as a series of ordinary differential equations. For either representation it will be possible to trace a possible evolution of the system or to solve the model numerically. The latter could allow a biologist to predict a key value at a specific time, such as the concentration of a particular molecule after ten minutes.A unique feature of the BioSPA language will be that it will also be possible to systematically prove properties of models in the language in order to ensure that they represent the system which the biologists wish to study. This strong, well-designed language will help to ensure the correctness of biological research and the validity of its results, with attendant benefits for medical and pharmaceutical research leading to improvements in the prevention and treatment of illness.