A linear collision avoidance example [5][8][12].

Let gap, vr, vl and ar respectively represent the distance between the two cars (di-1-di in the original paper), the velocity of the rear car (di'), the velocity of the leading car (di-1') and the acceleration of the rear car (di"). By using these variables and restricting vl by v1' >= -2/\vl' <= -0.5 we transformed the original higher-order differential equation into a four-dimensional differential (in)equation of order one.

We set the state space to [0,4]×[0,2]×[0,2] ×[-2,-0.5], and we want to verify that gap>0 when starting from gap=1,vr=2,vl=2 and ar=-0.5.

Input file