Autonomous Driving of Two Cars
We consider two autonomous cars, moving in the 2-dimensional plane: one (i.e., leader) drives according to its own scenario, and the other follows the leader (adapted from [1]). The controller of the autonomous cars controls the behavior of the followers. We consider a linear dynamics model and a nonlinear polynomial dynamics model.
Linear Dynamics. Figure [1] shows a hybrid automaton of the linear dynamics model. The following car is placed at $(x_i, y_i)$ with a velocity of $v_i$. The car moves with a direction $\theta_i$ and its steering angle is $\phi_i$. The controller changes the direction of the follower, according to its position: if the follower is to the left of the leader, the controller rotates the follower counter-clockwise ($\textsf{CC}$). If the follower is to the right of the leader, the controller rotates the follower clockwise ($\textsf{C}$). Otherwise, the follower goes straight ($\textsf{S}$). For simplicity, we consider the constant dynamics for the position of the follower car as follows:
\begin{align*}
\dot{x}_1 &= 3,& \dot{y}_1 &= 0 & \textsf{(S)} \\
\dot{x}_1 &= 1.5,& \dot{y}_1 &= 3,& \textsf{(CC)} \\
\dot{x}_1 &= 1.5,& \dot{y}_1 &= -3,& \textsf{(C)} \\
\end{align*}
Table [1] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $(\lozenge_{[3,5]}y_2 - y_1 \leq 5) \, \mathbf{U}_{[2, 10]} \, y_2 - y_1 \geq 8$ | For some time point in interval $[3, 5]$, $y_2$ is less than or equal to $y_1 + 5$ until $y_2$ is greater than or equal to $y_1 + 8$ for time interval $[2, 10]$. |
| $\textsf{f2}$ | $\lozenge_{[3,10]}(\square_{[5, 15]} \, x_2 - x_1 \geq -2)$ | For some time point in interval $[3, 10]$, $x_2$ is always greater than or equal to $x_1 - 2$ for time interval $[5, 15]$. |
| $\textsf{f3}$ | $(\square_{[2, 5]} \, y_2 - y_1 \leq 4) \, \mathbf{R}_{[0,10)} \, x_2 - x_1 \geq 4$ | For some time point in interval $[0, 10)$, $x_2$ is greater than or equal to $x_1 + 4$ until $y_2$ is less than or equal to $y_1 - 4$ during 3 time units. |
Table 1: STL properties for the linear model
Nonlinear Polynomial Dynamics. The relative distance of the following car $(r_x, r_y)$ depends on
the modes of the car ($\textsf{CxCy}$, $\textsf{CxFy}$, $\textsf{FxCy}$, and $\textsf{FxFy}$) and
its velocity $(v_{x}, v_{y})$.
When the relative distance of the car is too far (or close), the car accelerates (or decelerates).
For each mode, we consider the following dynamics:
\begin{align*}
\dot{r}_x &= v_{x},& \dot{r}_y &= v_{y},& \dot{v}_{x} &= 1.2,& \dot{v}_{y} &= 1.4 & \textsf{(CxCy)} \\
\dot{r}_x &= v_{x},& \dot{r}_y &= v_{y},& \dot{v}_{x} &= 1.2,& \dot{v}_{y} &= -1.4 & \textsf{(CxFy)} \\
\dot{r}_x &= v_{x},& \dot{r}_y &= v_{y},& \dot{v}_{x} &= -1.2,& \dot{v}_{y} &= 1.4 & \textsf{(FxCy)} \\
\dot{r}_x &= v_{x},& \dot{r}_y &= v_{y},& \dot{v}_{x} &= -1.2,& \dot{v}_{y} &= -1.4 & \textsf{(FxFy)}
\end{align*}
Figure [2] shows a hybrid automaton of the polynomial model. Initially, the relative distance is close. The following car tries to maintain the distance within certain range according to the control logic.
Figure 2: A hybrid automaton of the autonomous car
Table [2] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $\square_{[0,4]} (v_x < -2 \rightarrow \lozenge_{[2,5]} r_x \leq -2)$ | For the first $4$ time units, if $v_x$ is less than $-2$, then $r_x$ is greater than or equal to $-2$ for some time in interval $[2, 5]$. |
| $\textsf{f2}$ | $(\lozenge_{[0,4]} r_y > 3) \mathbf{U}_{[0, 5]} (v_y > 1.5)$ | For some time point in interval $[0, 4]$, $r_y$ is greater than $3$ until $v_y$ is greater than $1.5$ for time interval $[0, 5]$. |
| $\textsf{f3}$ | $\lozenge_{[0,3]} (r_x \leq 5 \mathbf{U}_{[0, 5]} ix = false)$ | $r_x$ is less than or equal to $5$ until $ix$ become $false$ for time interval $[0, 5]$, for some time point in interval $[0, 3]$. |
Table 2: STL properties for the polynomial model
An STLmc Input Model
We use the STLmc language to describe the linear dynamics model (car-linear.model) as follows:
bool r; bool d;
[-100, 100] x1; [-100, 100] y1;
[-100, 100] x2; [-100, 100] y2;
# car1 : straight
{ mode: r = false; d = false;
inv: x2 - x1 <= 5;
y2 - y1 <= 5;
flow: d/dt[x1] = 3; d/dt[y1] = 0;
d/dt[x2] = 2; d/dt[y2] = 2;
jump: (y2 - y1) >= 3 =>
(and (r' = true) (d' = false)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
(y2 - y1) <= -3 =>
(and (r' = true) (d' = true)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
}
# car1 : up
{ mode: r = true; d = false;
inv: x2 - x1 >= -5;
y2 - y1 >= -5;
flow: d/dt[x1] = 1.5; d/dt[y1] = 3;
d/dt[x2] = 2; d/dt[y2] = 2;
jump: (and ((y2 - y1) <= 1)
((y2 - y1) >= -1)) =>
(and (r' = false) (d' = false)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
(y2 - y1) <= -3 =>
(and (r' = true) (d' = true)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
}
# car1 : down
{ mode: r = true; d = true;
inv: x2 - x1 >= -5;
x2 - x1 <= 5;
flow: d/dt[x1] = 1.5; d/dt[y1] = -3;
d/dt[x2] = 2; d/dt[y2] = 2;
jump: (and ((y2 - y1) <= 1)
((y2 - y1) >= -1)) =>
(and (r' = false) (d' = false)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
(y2 - y1) >= 3 =>
(and (r' = true) (d' = false)
(x1' = x1) (y1' = y1)
(x2' = x2) (y2' = y2));
}
init: not(r); not(d);
0 <= x1; x1 <= 1; 2 <= x2; x2 <= 3;
0 <= y1; y1 <= 1; 2 <= y2; y2 <= 3;
proposition:
# bound: 20, timebound: 40
goal:
[f1]: (<> [3, 5] (y2 - y1) <= 5) U[2, 10] ((y2 - y1) >= 8); # threshold: 0.1
[f2]: [] [3, 10] (<>[5, 15] ((x2 - x1) >= -2)); # threshold: 0.5
[f3]: ([][2, 5] (y2 - y1 <= 4)) R [0, 10) ((x2 - x1) >= 4); # threshold: 1.0
We use the STLmc language to describe the polynomial dynamics model (car-poly.model) as follows:
bool ix; bool iy;
[-40, 40] rx; [-40, 40] ry;
[-30, 30] vx; [-30, 30] vy;
# acc, acc
{ mode: ix = true; iy = true;
inv: rx < 20; ry < 20;
vx < 8; vy < 8;
flow: d/dt[rx] = vx; d/dt[ry] = vy;
d/dt[vx] = 1.2; d/dt[vy] = 1.4;
jump: (and (rx >= 3) (ry < 3)) =>
(and (ix' = false) (iy' = true)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx < 3) (ry >= 3)) =>
(and (ix' = true) (iy' = false)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
}
# car1 : acc, dec
{ mode: ix = true; iy = false;
inv: rx < 20; ry > -20;
vx < 8; vy > -8;
flow: d/dt[rx] = vx; d/dt[ry] = vy;
d/dt[vx] = 1.2; d/dt[vy] = -1.4;
jump: (and (rx >= 3) (ry >= 3)) =>
(and (ix' = false) (iy' = false)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx >= 3) (ry < 3)) =>
(and (ix' = false) (iy' = true)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
}
# car1 : dec, acc
{ mode: ix = false; iy = true;
inv: rx > -20; ry < 20;
vx > -8; vy < 8;
flow: d/dt[rx] = vx; d/dt[ry] = vy;
d/dt[vx] = -1.2; d/dt[vy] = 1.4;
jump: (and (rx < 3) (ry < 3)) =>
(and (ix' = true) (iy' = true)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx >= 3) (ry >= 3)) =>
(and (ix' = false) (iy' = false)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx < 3) (ry >= 3)) =>
(and (ix' = true) (iy' = false)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
}
# car1 : dec, dec
{ mode: ix = false; iy = false;
inv: rx > -20; ry > -20;
vx > -8; vy > -8;
flow: d/dt[rx] = vx; d/dt[ry] = vy;
d/dt[vx] = -1.2; d/dt[vy] = -1.4;
jump: (and (rx < 3) (ry < 3)) =>
(and (ix' = true) (iy' = true)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx >= 3) (ry < 3)) =>
(and (ix' = false) (iy' = true)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
(and (rx < 3) (ry >= 3)) =>
(and (ix' = true) (iy' = false)
(rx' = rx) (ry' = ry)
(vx' = 0) (vy' = 0));
}
init: not(ix); not(iy);
0 <= rx; rx <= 1; -2.5 <= vx; vx <= -2;
0 <= ry; ry <= 1; -2.5 <= vy; vy <= -2;
proposition:
[pix]: ix;
# bound: 10, timebound: 10, solver: yices
goal:
[f1]: [][0,4] (vx < -2 -> <>[2,5] rx <= -2); # threshold: 0.5
[f2]: (<>[0, 4] ry > 3) U [0, 5] (vy > 1.5); # threshold: 2.0
[f3]: <>[0,3] (rx <= 5 U[0, 5] ~pix); # threshold: 0.1
Run
The following settings and example measurements use STLmc. A counterexample is a trace below the specified robustness threshold; a satisfied result applies only to the bounds shown. Timings vary by machine.
Linear Model.
stlmc ./car-linear.model -bound 20 -time-bound 40 -threshold 0.1 -goal f1 -solver yices -visualize -logic QF_LRA
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
20 | 40 | 40 | 0.1 | yices | one-step | 9.485 | violated at bound 8 |
f2 |
8 | 40 | 40 | 0.5 | yices | one-step | 5.313 | satisfied up to bound 8 |
f3 |
20 | 40 | 40 | 1 | yices | one-step | 24.100 | violated at bound 11 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Polynomial Model.
stlmc ./car-poly.model -bound 10 -time-bound 10 -threshold 0.5 -goal f1 -solver cvc5 -visualize
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
10 | 10 | 10 | 0.5 | cvc5 | one-step | 19.281 | violated at bound 3 |
f2 |
10 | 10 | 10 | 2 | cvc5 | one-step | 14.477 | violated at bound 3 |
f3 |
10 | 10 | 10 | 0.1 | cvc5 | one-step | 22.031 | satisfied up to bound 10 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Visualization
The plot shows the f1 counterexample for car-linear.model
with the settings above. Its sampled robustness is compared with the threshold.
The plot shows the f1 counterexample for car-poly.model
with the settings above. Its sampled robustness is compared with the threshold.
Reference
[1]. Rajeev Alur. 2015. Principles of Cyber-Physical Systems. The MIT Press.