A stochastic hybrid process algebra

V. Galpin, J. Hillston and L. Bortolussi

Models and Logics for Quantitative Analysis (MLQA 2010), Edinburgh, 9 July, 2010


The process algebra HYPE was developed for the modelling of system with discrete and continuous behaviour. We now extend HYPE with stochastic behaviour to broaden its applicability. In HYPE, events are categorised as urgent which means they must occur as soon as the condition governing them becomes true; or as non-urgent meaning that they happen at some unspecified point in the future. In stochastic HYPE, we remove the second option and introduce stochastic events which have associated exponential distributions. HYPE models can be interpreted as hybrid automata, whereas stochastic HYPE models require a more expressive semantics, namely Transition Driven Stochastic Hybrid Automata, a subset of Piecewise Deterministic Markov Processes.

We illustrate the use of stochastic HYPE by modelling delay-tolerant networks. These networks do not always have end-to-end connectivity and hence nodes in the network need additional storage for packets (bundles in delay-tolerant network terminology) that cannot be forwarded due to lack of connectivity. We describe individual buffer components made up of input and output subcomponents, and compose these to form the network model. Simulations illustrate the effect of different buffer sizes on the number of dropped packets.

Poster - PDF

Back to Publications page