COMPOSITIONAL ANALYSIS OF MARKOVIAN PROCESS ALGEBRA (CAMPA)

定量方法对于设计信息通信技术、通信网络和其他物流领域（如业务流程和医疗保健系统）的高效系统至关重要。但是，生成的模型需要对设计人员（而不仅仅是性能专家）可用，并且要高效。一个充分表达的形式主义是需要的，它可以在高水平的描述中指定模型，也可以促进可分离的，因此有效的数学解决方案。随机过程代数（SPA）是一种有可能满足这些要求的形式体系。解决状态空间爆炸问题的一种方法是利用所谓的产品形式解决方案，这是所有组合建模技术所共有的。本质上，乘积形式是分解后的解，其中系统的总体稳态分布可以通过将各组分的边际分布相乘得到。乘积形式的解决方案通常可以由反向过程的性质来定义，哈里森的开创性结果，被称为反向复合代理定理（RCAT）[15]，给出了一种在组件级别（在简单指定的条件下）生成马尔可夫过程代数模型的反向过程的方法，而不依赖于底层的连续时间马尔可夫链。这导致了对以前单独考虑的一系列产品形式结果的新理解，以及对新产品形式的新理解。它也使得分解解的机械推导，不仅具有精确的乘积形式的模型，而且在某种（定量）意义上几乎具有乘积形式的模型的潜在有界近似。该申请与EPSRC资助的SPARTACOS补助金（EP/D047587/1）密切相关，目前由Harrison持有。当前的应用程序将通过考虑“几乎”具有产品形式解决方案的模型来补充和扩展SPARTACOS中的工作，在某种意义上是精确指定的，以及服从于非产品形式分解的模型，这不是SPARTACOS项目的一部分。（SPARTACOS本身也考虑响应时间分布，更高的矩，离散时间和流体模型。）这个项目的主要部分将是促进托马斯博士对帝国理工学院的长期研究访问。

Quantitative methods are vital for the design of efficient systems in ICT, communication networks and other logistical areas such as business processes and healthcare systems. However, the resulting models need to be both accessible to the designer, rather than only to the performance specialist, and efficient. A sufficiently expressive formalism is needed that can specify models at a high level of description and also facilitate separable and hence efficient mathematical solutions. Stochastic process algebra (SPA) is a formalism that has the potential to meet these requirements. One approach to tackling the state space explosion problem common to all compositional modelling techniques is through the exploitation of, so called, product-form solutions. Essentially, a product-form is a decomposed solution where the overall steady state distribution of the system can be found by multiplying the marginal distributions of the components. product-form solutions can generally be defined by properties of the reversed process and Harrison's seminal result, known as the Reversed Compound Agent Theorem (RCAT) [15], gives a method for generating the reversed process of a Markovian process algebra model at the component level (under simply specified conditions), without recourse to the underlying continuous time Markov chain. This has led to new understanding of a range of product-form results that were previous considered separately, as well as to new product-forms. It also enables a mechanical derivation of decomposed solutions, not only of models with an exact product-form, but also potentially bounded approximations for models which almost have a product-form in a certain (quantitative) sense. This application is closely related to the EPSRC funded SPARTACOS grant (EP/D047587/1), currently held by Harrison. This current application will complement and extend work in SPARTACOS by considering models which 'almost' have a product-form solution, in a sense to be specified precisely, and models which are subject to a non-product-form decomposition, which has not been part of the SPARTACOS pro ject. (SPARTACOS itself also considers response time distributions, higher moments, discrete time and fluid models.) The principal part of this pro ject will be in facilitating an extended research visit to Imperial College by Dr Thomas.