(de-)Composed And More: Eager and Lazy Specifications (CAMELS) for Stochastic Hybrid Systems

Different stochastic extensions of hybrid automata have been proposed in the past, with unclear expressivity relations between them. In previous work, we related these modelling languages with regard to two alternative (composed and decomposed) approaches to extend hybrid automata with stochastic choices of discrete events and their time points. This paper presents the so-called CAMELS classification, which additionally distinguishes between lazy and eager modelling. The former does not restrict how delays are chosen and performs resampling in case no discrete event is possible at the scheduled jump time. The latter guarantees that discrete events are only scheduled at times when they are enabled. We further distinguish between an eager predictive specification, which uses precomputations of all possible delays, and an eager non-predictive specification, which samples enabling durations instead of global delays. These distictions result in five model classes which we compare regarding their expressivity, and discuss how available modelling formalisms for stochastic hybrid automata from the literature can be categorized within the CAMELS classification.