COMPOSITIONAL ANALYSIS OF MARKOVIAN PROCESS ALGEBRA (CAMPA)

点击翻译按钮获取中文摘要

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.