A Railroad Gate Controller

There are a gate and a gate controller with a crossing bar on a circular railroad track and a train moves on the track. The gate controller opens (or closes) the crossing bar when the train approaches to (or leaves from) the gate (adapted from [1]). Figure [1] shows a hybrid automaton for this system. The position of the crossing bar $p_b$ from the ground changes according to the velocity of bar $v_b$, depending on the modes ($\textsf{Far}$, $\textsf{Approach}$, $\textsf{Close}$, and $\textsf{Past}$) of the gate controller and the distance $x$, between the gate and the train.

Fig.1: A hybrid automaton of the railroad gate controller

For each mode, we consider the following dynamics: \begin{align*} \dot{x} &= -30,& \dot{p}_b &= v_b,& \dot{v}_b &= 0 & \textsf{(Far)} \\
\dot{x} &= -5,& \dot{p}_b &= v_b,& \dot{v}_b &= 0.3 & \textsf{(Approach)} \\
\dot{x} &= -5,& \dot{p}_b &= v_b,& \dot{v}_b &= 0.5 & \textsf{(Close)} \\
\dot{x} &= -5,& \dot{p}_b &= v_b,& \dot{v}_b &= -1 & \textsf{(Past)} \end{align*}

Table [1] shows the STL properties.

Label	STL formula	Description
$\textsf{f1}$	$\lozenge_{[0,5]} ((p_b \geq 40) \mathbf{U}_{[1,8]} (x < 40))$	For some time point in interval $[0,5]$, $p_b$ is greater than or equal to $40$, until $x$ is less than $40$ during time interval $[1, 8]$.
$\textsf{f2}$	$\lozenge_{[0,4]} (x < 50 \to \square_{[2,10]} (p_b > 40))$	Within $4$ time units, if $x$ is less than $50$, then $p_b$ is greater than $40$ for time interval $[2, 10]$.
$\textsf{f3}$	$\square_{[0,5)} ((x < 50) \mathbf{U}_{[2,10]} (p_b > 5))$	During time interval $[0, 5)$, $x$ is less than $50$ until $p_b$ is greater than $5$ within time interval $[2, 10]$.

Table.1: STL properties for the railroad gate controller

---

An STLmc Input Model

We use the STLmc language to describe the railroad model (railroad.model) as follows:

bool a;    bool b;
[-20, 100] x; [0, 90] pb; [-50, 50] vb;
# far
{ mode: a = false; b = false;
  inv:  x > 60;
  flow: d/dt[x] = -30; 
        d/dt[pb] = vb;
        d/dt[vb] = 0;
  jump: x < 80 => (and (a' = a) (b' = true) 
                       (pb' = pb) (x' = x) 
                       (vb' = 6));
        x < 70 => (and (a' = true) (b' = b) 
                       (pb' = pb) 
                       (x' = x) (vb' = 8));
}
# approach
{ mode: a = false; b = true;
  inv:  x > 20;
  flow: d/dt[x] = -5; 
        d/dt[pb] = vb;
        d/dt[vb] = 0.3;
  jump: x < 80 => (and (a' = true) (b' = false) 
                       (pb' = pb) 
                       (x' = x) (vb' = vb));
}
# close
{ mode: a = true; b = false;
  inv:  x > 10;
  flow: d/dt[x] = -5; 
        d/dt[pb] = vb;
        d/dt[vb] = 0.5;
  jump: x < 20 => (and (a' = a) (b' = true)
                       (pb' = pb) 
                       (x' = x) (vb' = -4));
}
# past
{ mode: a = true; b = true;
  inv:  x > -10;
  flow: d/dt[x] = -5; 
        d/dt[pb] = vb;
        d/dt[vb] = -1;
  jump: (x < 0) => (and (a' = false) 
                        (b' = false) 
                        (pb' = pb) (vb' = 0)
                        (x' = 100 + x));
}
init: a = false; 89 <= x; x <= 90;
      b = false; 0 <= pb; pb <= 0.5; 
      vb = 0;

proposition:

# bound: 10, timebound 20, solver: yices
goal:
  [f1]: <>[0, 5] ((pb >= 40) U[1, 8] (x < 40));	  # threshold: 1.0
  [f2]: <>[0, 4](x < 50 -> [][2,10] pb > 40);	  # threshold: 5.0
  [f3]: [][0.0,5.0) ((x < 50) U[2, 10] (pb > 5)); # threshold: 4.0

---

Run

For the input model, we use a time bound $\tau = 20$ 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 = 1.0$, $\epsilon_2 = 5.0$, and $\epsilon_3 = 4.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 $\textsf{f1}: \lozenge_{[0,5]} ((p_b \geq 40) \mathbf{U}_{[1,8]} (x < 40))$ at bound $5$ with respect to $\epsilon_1=1.0$ in $4$ seconds using yices.

stlmc ./railroad.model -bound 10 -time-bound 20 -threshold 1.0 \
      -goal f1 -solver yices -visualize

Label	$\epsilon$	$| \Psi |$	Time	Result	$k$	Alg.
$\textsf{f1}$	$1.0$	$2.3$	$3.43$	$\bot$	$5$	$\textsf{1-step}$
$\textsf{f2}$	$5.0$	$3.8$	$0.86$	$\top$	-	$\textsf{1-step}$
$\textsf{f3}$	$4.0$	$1.9$	$2.83$	$\bot$	$4$	$\textsf{1-step}$

Table.2: Verification results of the STL properties for the railroad gate controller

---

Visualization

Fig.2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 1.0$)

Figure [2] shows the visualization graphs generated for $\textsf{f1} = \lozenge_{[0, 5]} (p_b \geq 40 \, \mathbf{U}_{[1, 8]} \, x < 40)$ with the subformulas: \begin{align*} \textsf{f1}_{\textsf{1}} = p_b \geq 40 \, \mathbf{U}_{[1, 8]} \, x < 40 \qquad \textsf{f1}_{\textsf{2}} = p_{b} \geq 40 \qquad \textsf{f1}_{\textsf{3}} = x < 40 \end{align*}

The robustness degree of $\textsf{f1}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f1}_{\textsf{1}}$ is always less than $\epsilon$ in the interval $[0, 5]$, which is because the degree of $\textsf{f1}_{\textsf{2}}$ is less than $\epsilon$ from the starting time $1$ of the interval $[1, 13] = [0, 5] + [1, 8]$.

---

Reference

[1]. Henzinger T.A. (2000) The Theory of Hybrid Automata. In: Inan M.K., Kurshan R.P. (eds) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol 170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59615-5_13