What Is Decidable About Low Dimensional Hybrid Systems?

Olga Tveretina's journal club session, where she will present herself and Andrei Sandler's work.

A hybrid system is a dynamic system that exhibits both continuous and discrete behaviour, and the number of its dimensions is determined by the number of the continuous variables. The hybrid system paradigm is a useful tool for describing a wide range of real-world applications. Examples come from robotics, avionics, biological networks, chemical processes, etc. Most of the hybrid systems are safety critical. Formally, verifying safety properties of hybrid systems consists of construction of a set of reachable states and checking whether this set intersects with a set of unsafe states. Therefore, one of the most fundamental problems in the analysis of hybrid systems is the reachability problem. The reachability problem is known for being difficult, and it is only decidable for special kinds of hybrid systems. Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, it is far from being resolved. Asarin, Mysore, Pnueli and Schneider defined some classes of low dimensional hybrid systems lying on the boundary between decidable and undecidable systems in their seminal paper "Low dimensional hybrid systems – decidable, undecidable, don’t know (Asarin et al., 2012)", and for which decidability is unknown. In this talk, Olga will present an overview of the area and discuss the recent work on the decidability of reachability for a class of hybrid systems due to Asarin, Mysore, Pnueli and Schneider.

Date: 15/03/2019
Time: 16:00
Location: D118

Share this post on: Twitter| Facebook| Google+| Email