Comparing Two Approaches to Include Stochasticity in Hybrid Automata

TL;DR

This paper compares two formal methods for incorporating stochasticity into hybrid automata, analyzing their expressivity and categorizing existing stochastic extensions in the literature.

Contribution

It formalizes and compares two approaches to stochastic hybrid automata, clarifying their expressivity relations and providing a structured categorization of existing models.

Findings

Decomposed scheduling uses stochastic races for event timing.

Composed scheduling samples event timing before choosing the event.

The two approaches have distinct expressivity properties.

Abstract

Different stochastic extensions of hybrid automata have been proposed in the past, with unclear expressivity relations between them. To structure and relate these modeling languages, in this paper we formalize two alternative approaches to extend hybrid automata with stochastic choices of discrete events and their time points. The first approach, which we call decomposed scheduling, adds stochasticity via stochastic races, choosing random time points for the possible discrete events and executing a winner with an earliest time. In contrast, composed scheduling first samples the time point of the next event and then the event to be executed at the sampled time point. We relate the two approaches regarding their expressivity and categorize available stochastic extensions of hybrid automata from the literature.