Fluid Approximation for Stochastic Process Algebras and Stochastic Model Checking.
Stochastic process algebras have been successfully applied to quantitative evaluation of systems for nearly two decades. Such models may be used to analyse the timeliness of response or utilisation of resources within systems.
By modelling systems as collections of individual agents, the process algebra approach allows the modeller to capture the exact form of interactions and constraints between entities. However this approach suffers from the problem of state space explosion making analysis inefficient or even infeasible. In recent years there has therefore been interest in using mean-field or fluid approximation techniques in this context.
In this talk I will discuss recent work on novel semantics for the stochastic process algebra PEPA which allow a fluid approximation to be derived in addition to a symbolic representation of the discrete state space. Moreover I will explain how the semantics allow the necessary structural properties to be established for the language, rather than model by model, allowing the approximation to be applied automatically to suitable models. I will go on to explain recent preliminary work on extending the scope of fluid approximations to stochastic model checking, presenting an algorithm to establish properties of an individual within a population, taking advantage of the asymptotic independence of entities in the mean field results.