Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata

Abstract

In this paper we present a modelling formalism for dynamic networks
of stochastic hybrid automata. In particular, our formalism is based on primitives
for the dynamic creation and termination of hybrid automata components during
the execution of a system. In this way we allow for natural modelling of concepts
such as multiple threads found in various programming paradigms, as well as the
dynamic evolution of biological systems.
We provide a natural stochastic semantics of the modelling formalism based on re-
peated output races between the dynamic evolving components of a system. As
specification language we present a quantified extension of the logic Metric Tempo-
ral Logic (MTL). As a main contribution of this paper, the statistical model checking
engine of U PPAAL has been extended to the setting of dynamic networks of hybrid
systems and quantified MTL. We demonstrate the usefulness of the extended for-
malisms in an analysis of a dynamic version of the well-known Train Gate example,
as well as in natural monitoring of a MTL formula, where observations may lead to
dynamic creation of monitors for sub-formulas.