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.

model

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}$ $\square_{[0,14]}(x\leq94)$ During the first 14 time units, the train position stays at or below 94.
$\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,2)}((x<50)\mathbf{U}_{[1,5]}(p_b>5))$ At every time in $[0,2)$, $p_b>5$ must hold after 1 to 5 time units, with $x<50$ until then.

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:

# Pass the per-goal analysis settings listed on the benchmark page explicitly.
goal:
  [f1]: [][0, 14] (x <= 94); # threshold: 0
  [f2]: <>[0, 4](x < 50 -> [][2,10] pb > 40);	  # threshold: 5.0
  [f3]: [][0, 2) ((x < 50) U[1, 5] (pb > 5)); # threshold: 4.0

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.

stlmc ./railroad.model -bound 8 -time-bound 16 -time-horizon 16 -threshold 0 -goal f1 -solver cvc5 -visualize
Goal Max bound Time bound Time horizon Threshold Solver Engine Seconds Result
f1 8 16 16 0 cvc5 one-step 3.112 violated at bound 5
f2 10 20 20 5 yices one-step 10.972 satisfied up to bound 10
f3 10 8 8 4 cvc5 one-step 25.339 violated at bound 3

Select -goal, -bound, -time-bound, -time-horizon, and -threshold according to the row.

For f2, select -solver yices; the other two goals use CVC5.

Visualization

The plot shows the f1 counterexample for railroad.model with the settings above. It passes through far, close, past, far, and approach modes: four physical mode changes. The train position is reset by x' = 100 + x when it returns from past to far; this exceeds the safety limit 94. The additional partition point near time 14.11 is not a mode change. The safety property covers the first 14 time units; the plotted execution continues to time 16. Its sampled robustness is compared with the threshold.

Open the interactive plot.

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