COMPOSITIONAL ANALYSIS OF MARKOVIAN PROCESS ALGEBRA (CAMPA)

定量方法对于ICT、通信网络和其他物流领域（如业务流程和医疗保健系统）的高效系统设计至关重要。然而，所产生的模型需要对设计师（而不仅仅是性能专家）和高效都是可访问的。一个充分表达的形式主义是必要的，可以指定模型在一个高层次的描述，也有利于分离，因此有效的数学解决方案。随机进程代数（SPA）是一种形式主义，有可能满足这些要求。解决所有组合建模技术共同的状态空间爆炸问题的一种方法是通过利用所谓的产品形式解决方案。从本质上讲，乘积形式是一个分解的解决方案，其中系统的整体稳态分布可以通过乘以组件的边缘分布来找到。乘积形式的解通常可以由反向过程的性质来定义，哈里森的开创性结果，称为反向复合代理定理（RCAT）[15]，给出了一种在组件级别（在简单指定的条件下）生成马尔可夫过程代数模型的反向过程的方法，而无需求助于底层的连续时间马尔可夫链。这导致了对以前单独考虑的一系列产品形式结果的新理解，以及新的产品形式。它还使机械推导的分解的解决方案，不仅具有确切的产品形式的模型，但也可能有界的近似模型，几乎有一个产品的形式在一定的（定量）意义上。该申请与EPSRC资助的SPARTACOS赠款（EP/D 047587/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.