|# of variables||# of modes||# of jumps|
|Type||Continuous dynamics||Guards & Invariants||Resets|
|hybrid||linear polynomial||hyperplane & half-space||identity|
The considered benchmark presented in Fig.1(a) consists of two tanks. The liquid in the first tank comes from two outside sources: a constant inflow source and a second source equipped with a controlled valve valve1, with flows and respectively. A drain placed at the bottom of tank 1 allows the liquid to flow into tank 2 with flow .
Tank 2 is itself equipped with two drains. In the first one a pump is placed to assure a constant liquid outflow whereas the flow in the second one is controlled by an electro-valve valve2.Both valves can take the states On/Off. This results consequently in four possible discrete modes for the hybrid automaton. The liquid levels in tank i is given by .
The dynamics of the above system is defined by the following differential equations:
We consider an initial set of
and the starting location , a time horizon , and a time step . The set of bad states are all states, where .
Fig.2 shows the flowpipes computed for the above-mentioned parameters using a) HyReach and b) SpaceEx. The results given in Fig. 2 show tightness difference between the two obtained flowpipes, although both proposed tools are based on the same reachability analysis technique using support functions.
Figure 2: Flowpipe of the two-tank system
 J. Lygeros. Lecture notes on hybrid systems. Technical Report, 2004.
 I. A. Hiskens. Stability of limit cycles in hybrid systems. In Proceedings of the 34th Hawaii International Conference on System Sciences (HICSS’01), pages 163-328, IEEE, 2001.
 A. Girard. Reachability of Uncertain Linear Systems Using Zonotopes. In Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC’05), Volume 3414 of LNCS, pp 291-305, Springer, 2005.