Stochastic HYPE is a process algebra for modelling natural and artificial systems that exhibit stochastic, continuous and discrete behaviour. It extends the hybrid process algebra HYPE with events that have exponentially-distributed durations. The semantics of HYPE systems are given by Transition-Driven Stochastic Hybrid Automata, a subset of Piecewise Deterministic Markov Processes. This presentation will introduce stochastic HYPE, and show how it is possible to ascertain that a stochastic HYPE model does not have infinite sequences of discrete behaviour through an syntactic analysis of the model. Such models are described as well-behaved. This technique will be illustrated with the example of a railway crossing. This is joint work with Jane Hillston (University of Edinburgh) and Luca Bortolussi (University of Trieste).
Slides - PDF