In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata


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.

ACM SIGLOG News, 6(1)
Mingshuai Chen
Mingshuai Chen
ZJU100 Young Professor

My research interests include formal verification, programming theory, and logical aspects of computer science.