Process Algebra Approaches to Collective Dynamics

这个科学研究项目的目的是帮助理解当我们可以模拟个体的行为时，我们如何预测种群的动态行为。在许多科学领域都有这样一个问题的应用领域，但其中最重要的是在生物学领域。生物学家研究细胞，试剂，分子和分子复合物，以获得对生长和变化的见解。在这里，仔细定义的模型越来越重要，因为越来越多的生物学研究正在使用基于计算机的分析。这种形式的研究补充了生物学研究，后者是传统的实验室科学，基于受控实验，数据收集和观察。模型允许生物学家尝试理解他们观察到的数据，形成假设，然后在进一步的实验中进行测试。他们的研究成果激发了新药物和治疗方法的设计，这些药物和治疗方法可以对抗疾病，改善人类和动物的健康。科学家需要语言来有效和明确地进行交流。生物学家开发的模型通常用莱布尼茨发明的微积分的数学符号写成微分方程。虽然这种符号有许多优点，但它并不总是最直观的使用，并且可以远离所描述的细胞过程。因此，生物学家一直在研究其他科学领域的其他系统描述语言的使用，计算机科学在形式语言设计方面比其他科学有更多的经验。在计算机科学中，形式语言被用于各种目的，其中之一是程序的设计和验证。已用于此目的的一类语言是进程代数，它以及描述系统的功能，配备了比较系统和证明它们的属性的技术。诸如进程代数之类的形式语言并不像人类语言那样自然进化。相反，他们需要仔细设计。这个奖学金将带来的好处，计算机科学的经验，在正式语言设计的一个新的过程代数建模生物系统，语言BioSPA的设计。这种新语言的一个关键方面将是它使用数学量化的随机性。在每一个生物中，都有一个可控的随机性，因为生物是由化学反应驱动的。由于热分子运动固有的随机性，化学反应系统随机演化。BioSPA语言将得到软件工具的支持，使生物学家能够以多种方式查看他们的模型。例如，作为马尔可夫过程，在许多不同状态之间随机移动的数学过程，或者作为一系列常微分方程。对于任何一种表示，都有可能追踪系统的可能演化或用数值方法求解模型。后者可以让生物学家在特定时间预测一个关键值，比如十分钟后特定分子的浓度。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.