Stochastic process algebras, where actions have randomly distributed durations, can be used to model the dynamic behaviour of biological systems. These models use a direct analogy between the rates assigned to actions and the rates associated with reactions. The main methods of analysis for stochastic process algebra models are stochastic simulation and deterministic evaluation via ordinary differential equations, since neither require the overhead of transition system construction and the attendant state space explosion in the case of high molecular counts. The stochastic process algebra Bio-PEPA, developed specifically for systems biology, permits concentrations to be discretised and molecular counts to be stratified, reducing the number of states and offering access to transition-system-based analysis techniques. Semantic equivalences in the process algebra tradition are defined over transitions systems and hence Bio-PEPA provides the opportunity to explore these.
A semantic equivalence captures the idea of two models having the same behaviour, for a given notion of behaviour. If the equivalence is a congruence with respect to the operators of the process algebra,then one model can be substituted for another, allowing for a more compact model to replace a larger model. By identifying behaviours, it is possible to develop a range of equivalences, and some are now described.
Compression bisimilarity is based on the idea that two discretisations of a model should have the same behaviour. It is shown that for discretisations with sufficient numbers of discrete levels that compression bisimilarity holds for individual species components and cooperations of species components.
A parameterised equivalence, g-bisimilarity can generate many different equivalences, each determined by the function g which isolates information of interest. Its use is illustrated with an example of a model where two distinct but similar species are grouped into one species. Congruence is proved under certain reasonable conditions on the function g.
Fast-slow bisimilarity is motivated by the Quasi-Steady-State assumption and abstracts from the details of fast reactions. It is applied to competitive behaviour. Congruence is shown for the cooperation operator when no fast reactions are shared.
In conclusion, Bio-PEPA allows the investigation of semantic equivalences in systems biology, and these equivalences can successfully equate models in terms of their behaviour.
Poster - PDF