Abstract

Stochastic process algebra (SPA) is a formalism developed over the last decade that can describe rigorously both the qualitative (functional) and quantitative (performance-related) behaviour of systems of interacting processes. The principal advantage of this algebraic approach to modelling is the property of compositionality possessed by all SPAs. This means that two or more fully specified systems can be combined together (as subsystems) into a more complex system in a simple way---both syntactically and semantically. The behaviour of the subsystems is not affected, except where they are explicitly connected to each other. Compositionality allows the properties of complex systems to be analysed in a hierarchical, inductive way and offers the prospect of efficient performance models, although the latter does not come automatically.

A new approach to deriving efficient, product-form solutions in Markovian process algebra (MPA) using properties of reversed processes will be presented. The compositionality of MPAs is directly exploited, allowing a large class of hierarchically constructed systems to be solved for their state probabilities at equilibrium. New results on both reversed stationary Markov processes and MPA itself are included, resulting in a mechanisable proof in MPA notation of Jackson's theorem for product-form queueing networks. Several examples are used to illustrate the approach.