Process Algebra Approaches to Collective Dynamics

这个科学研究计划的目的是帮助理解当我们可以对个人的行为进行建模时，我们如何预测一个群体的动态行为。这样的问题在许多科学领域都有应用领域，但最重要的是生物学领域。生物学家研究细胞、试剂、分子和分子复合体，以便洞察生长和变化。在这里，仔细定义的模型变得越来越重要，因为现在越来越多的生物学研究正在使用基于计算机的分析来完成。这种研究形式是对生物学研究的补充，生物学研究是基于对照实验、数据收集和观察的传统实验室科学。模型允许生物学家试图理解他们观察到的数据，形成假说，然后在进一步的实验中进行检验。他们的研究发现启发了抗击疾病和改善人类和动物健康的新药和治疗方法的设计。科学家需要语言来进行有效和明确的沟通。生物学家开发的模型通常用莱布尼茨发明的微积分的数学符号写成微分方程式。虽然这种记法有许多优点，但它并不总是最直观的使用方法，而且可以与所描述的细胞过程相去甚远。因此，生物学家一直在研究其他科学领域的其他系统描述语言的使用。计算机科学在形式语言设计方面比其他科学有更多的经验。在计算机科学中，形式语言被用于各种目的，其中之一是程序的设计和验证。用于这一目的的一类语言是进程代数，它除了用于描述系统的特征外，还配备了比较系统和证明系统性质的技术。像进程代数这样的形式语言不会像人类语言那样自然演化。相反，它们需要精心设计。这一奖学金将把计算机科学在形式语言设计方面的经验带到设计一种用于模拟生物系统的新进程代数--语言BioSPA。这种新语言的一个关键方面将是它使用了数学上量化的随机性。每一种生物都有一定数量的随机性，因为生物是由化学反应驱动的。由于热分子运动固有的随机性，化学反应系统的演化是随机的。BioSPA语言将得到软件工具的支持，这将允许生物学家以多种方式查看他们的模型。例如，作为马尔可夫过程，在若干不同状态之间随机移动的数学过程，或作为一系列常微分方程式。对于任何一种表示，都有可能跟踪系统的可能演变或以数字方式求解该模型。后者可以允许生物学家预测特定时间的关键值，例如10分钟后特定分子的浓度。BioSPA语言的一个独特特征是，还可以系统地证明该语言中的模型的性质，以确保它们代表生物学家希望研究的系统。这一强有力的、精心设计的语言将有助于确保生物研究的正确性及其结果的有效性，并随之而来的是医学和药物研究的好处，从而改善疾病的预防和治疗。

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.