Search

Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with automata capturing switching behavior. Since the introduction of the computational model more than a quarter of a century ago [Maler et al. 1992], its algorithmic verification has been an area of intense research. Within this note, which is dedicated to Oded Maler (1957--2018) as one of the inventors of the model, we are trying to delineate major lines of attack to the reachability problem for hybrid automata. Due to its relation to system safety, the reachability problem is a prototypical verification problem for hybrid discrete-continuous system dynamics.

Emerging smart technologies add elements of intelligence, cooperation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes. Hybrid automata, in their various flavours, have been suggested as a formal model accurately capturing CPS dynamics and thus facilitating exhaustive behavioural analysis of interacting CPSes with mathematical rigour.

Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. Various flavours of hybrid automata have been suggested as a means to formally analyse such dynamical systems, among them deterministic automata models facilitating reasoning about their normative behaviour, nondeterministic automata under a demonic interpretation supporting worst-case analysis, and stochastic variants enabling quantitative verification. In this article, we demonstrate that all these variants provide imprecise, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under uncertain observation of their environment due to, e.g., measurement error. We argue that even the most elaborate models of hybrid automata currently available ignore wisdom from metrology and game theory concerning environmental state estimation to be pursued by a rational player, which a control system obviously ought to constitute. We consequently suggest a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model.