Model checking stochastic hybrid systems
Ph.D. Thesis, Universität des Saarlandes
Downloads: pdf, bibURL: http://scidok.sulb.uni-saarland.de/volltexte/2013/5259/
Abstract. The interplay of random phenomena with discrete-continuous
dynamics deserves in- creased attention in many systems of growing importance.
Their verification needs to consider both stochastic behaviour and hybrid
dynamics. In the verification of classical hybrid systems, one is often
interested in deciding whether unsafe system states can be reached. In the
stochastic setting, we ask instead whether the probability of reaching
particular states is bounded by a given threshold. In this thesis, we consider
stochastic hybrid systems and develop a general abstraction framework for
deciding such problems. This gives rise to the first mechanisable technique
that can, in practice, formally verify safety properties of systems which
feature all the relevant aspects of nondeterminism, general continuous-time
dynamics, and probabilistic behaviour. Being based on tools for classical
hybrid systems, future improvements in the effectiveness of such tools
directly carry over to improvements in the effectiveness of our technique.
We extend the method in several directions. Firstly, we discuss how we can
handle continuous probability distributions. We then consider systems which
we are in partial control of. Next, we consider systems in which probabilities
are parametric, to analyse entire system families at once. Afterwards, we
consider systems equipped with rewards, modelling costs or bonuses. Finally,
we consider all orthogonal combinations of the extensions to the core model.