Stochastic model checking of the stochastic quality calculus

Abstract

The Quality Calculus uses quality binders for input to express strategies for continuing the computation even when the desired input has not been received. The Stochastic Quality Calculus adds generally distributed delays for output actions and real-time constraints on the quality binders for input. This gives rise to Generalised Semi-Markov Decision Processes for which few analytical techniques are available. We restrict delays on output actions to be exponentially distributed while still admitting real-time constraints on the quality binders. This facilitates developing analytical techniques based on stochastic model checking and we compute closed form solutions for a number of interesting scenarios. The analyses are applied to the design of an intelligent smart electrical meter of the kind to be installed in European households by 2020.