Reachability Analysis of a Class of Hybrid Gene Regulatory Networks.

In this work, we study the reachability analysis method of a class of hybrid systems called HGRN which is a special case of hybrid automata. The reachability problem concerned in this work is, given a singular state and a region (a set of states), to determine whether the trajectory from this singular state can reach this region. This problem is undecidable for general hybrid automata, and is decidable only for a restricted class of hybrid automata, but this restricted class does not include HGRNs. A priori, reachability in HGRNs is not decidable; however, we show in this paper that it is decidable in certain cases, more precisely if there is no chaos. Based on this fact, the main idea of this work is that if the decidable cases can be determined automatically, then the reachability problem can be solved partially. The two major contributions are the following: firstly, we classify trajectories into different classes and provide theoretical results about decidability; then based on these theoretical results, we propose a reachability analysis algorithm which always stops in finite time and answers the reachability problem partially (meaning that it can stop with the inconclusive result, for example with the presence of chaos).