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 = false); # threshold: 0.1
Run
Linear Model. For the linear input model, we use a time bound $\tau = 40$ and a discrete bound $N = 20$ as input parameters. Because the model has linear dynamics, we use $\textsf{yices}$ for an underlying solver with the default algorithm $\textsf{1-step}$. For the formulas $\textsf{f1}$, $\textsf{f2}$, and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 0.1$, $\epsilon_2 = 0.5$, and $\epsilon_3 = 1.0$, respectively.
STLmc finds counterexamples for $\textsf{f1}$ and $\textsf{f3}$, while $\textsf{f2}$ is safe. The following shows the command finding a counterexample for the STL formula $(\lozenge_{[3,5]}y_2 - y_1 \leq 5) \, \mathbf{U}_{[2, 10]} \, y_2 - y_1 \geq 8$ at bound $5$ with respect to $\epsilon_1=0.1$ in $8$ seconds using yices.
./stlmc ./car-linear.model -bound 20 -time-bound 40 -threshold 0.1 -goal f1 -solver yices -visualize
| Label | $\epsilon$ | $| \Psi |$ | Time | Result | $k$ | Alg. |
|---|---|---|---|---|---|---|
| $\textsf{f1}$ | $0.1$ | $2.5$ | $7.6$ | $\bot$ | $5$ | $\textsf{1-step}$ |
| $\textsf{f2}$ | $0.5$ | $10.8$ | $559.2$ | $\top$ | - | $\textsf{1-step}$ |
| $\textsf{f3}$ | $1.0$ | $2.5$ | $7.8$ | $\bot$ | $5$ | $\textsf{1-step}$ |
Table 3: Verification results of the STL properties for the linear model
Polynomial Model. For the polynomial input model, we use a time bound $\tau = 10$ and a discrete bound $N = 10$ as input parameters. Because the model has nonlinear polynomial dynamics, we use $\textsf{yices}$ for an underlying solver with the default algorithm $\textsf{1-step}$. For the formulas $\textsf{f1}$, $\textsf{f2}$, and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 0.5$, $\epsilon_2 = 2.0$, and $\epsilon_3 = 0.1$, respectively.
STLmc finds counterexamples for $\textsf{f1}$ and $\textsf{f2}$, while $\textsf{f3}$ is safe. The following shows the command finding a counterexample for the STL formula $\textsf{f1}: \square_{[0,4]} (v_x < -2 \rightarrow \lozenge_{[2,5]} r_x \leq -2)$ at bound $5$ with respect to $\epsilon_1=0.5$ in $8$ seconds using yices.
./stlmc ./car-poly.model -bound 10 -time-bound 10 -threshold 0.5 -goal f1 -solver yices -visualize
| Label | $\epsilon$ | $| \Psi |$ | Time | Result | $k$ | Alg. |
|---|---|---|---|---|---|---|
| $\textsf{f1}$ | $0.5$ | $2.2$ | $7.24$ | $\bot$ | $5$ | $\textsf{1-step}$ |
| $\textsf{f2}$ | $2.0$ | $1.7$ | $6.27$ | $\bot$ | $3$ | $\textsf{1-step}$ |
| $\textsf{f3}$ | $0.1$ | $7.3$ | $9.72$ | $\top$ | - | $\textsf{1-step}$ |
Table 4: Verification results of the STL properties for the polynomial model
Visualization
Linear Model.
Figure 3: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 0.1$)
Figure [3] shows the visualization graphs generated for $\textsf{f1} = (\lozenge_{[3,5]}y_2 - y_1 \leq 5) \, \mathbf{U}_{[2, 10]} \, y_2 - y_1 \geq 8$ with the subformulas: \begin{align*} \textsf{f1}_{\textsf{1}} &= (\lozenge_{[3, 5]} y_{2} - y_{1} \leq 5) \qquad \textsf{f1}_{\textsf{2}} = y_{2} - y_{1} \geq 8 \qquad \textsf{f1}_{\textsf{3}} = y_{2} - y_{1} \leq 5 \end{align*}
The robustness degree of $\textsf{f1}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f1}_{\textsf{2}}$ is always below $\epsilon$ in the interval $[5, 15] = [3, 5] + [2, 10]$. Note that, $\textsf{f1}_{\textsf{3}}$ is always greater than $\epsilon$ in the same time interval. Thus, the property is violated because $\textsf{f1}_{\textsf{2}}$ is false for the time interval $[5, 15]$.
Polynomial Model.
Figure 4: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 0.5$)
Figure [4] shows the visualization graphs generated for $\textsf{f1} = \square_{[0, 4]} (v_x < -2 \rightarrow \square_{[2, 5]} r_x \leq -2)$ with the subformulas:
\begin{align*}
\textsf{f1}_{\textsf{1}} &= v_x < -2 \rightarrow \lozenge_{[2, 5]} (r_x \leq -2) \qquad \textsf{f1}_{\textsf{2}} = \neg (v_{x} < -2) \qquad
\textsf{f1}_{\textsf{3}} = \lozenge_{[2, 5]} (r_{x} \leq -2) \\
\textsf{f1}_{\textsf{4}} &= r_{x} \leq -2 \qquad
\textsf{f1}_{\textsf{5}} = v_{x} < -2
\end{align*}
The robustness degree of $\textsf{f1}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f1}_{\textsf{1}}$ goes below $\epsilon$ in the interval $[0, 4]$, which is because both the degrees of $\textsf{f1}_{\textsf{2}}$ and $\textsf{f1}_{\textsf{3}}$ are less than $\epsilon$ in $[0, 4]$. The robustness degree of $\textsf{f1}_{\textsf{3}}$ is less than $\epsilon$ in $[0, 4]$, since the robustness degree of $\textsf{f1}_{\textsf{4}}$ is less than $\epsilon$ in $[2, 9] = [0, 4] + [2, 5]$.
Reference
[1]. Rajeev Alur. 2015. Principles of Cyber-Physical Systems. The MIT Press.