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 pb from the ground changes according to the velocity of bar vb, depending on the modes (Far, Approach, Close, and 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: ˙x=30,˙pb=vb,˙vb=0(Far)˙x=5,˙pb=vb,˙vb=0.3(Approach)˙x=5,˙pb=vb,˙vb=0.5(Close)˙x=5,˙pb=vb,˙vb=1(Past)

Table [1] shows the STL properties.

Label STL formula Description
f1 [0,5]((pb40)U[1,8](x<40)) For some time point in interval [0,5], pb is greater than or equal to 40, until x is less than 40 during time interval [1,8].
f2 [0,4](x<50[2,10](pb>40)) Within 4 time units, if x is less than 50, then pb is greater than 40 for time interval [2,10].
f3 [0,5)((x<50)U[2,10](pb>5)) During time interval [0,5), x is less than 50 until pb 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 τ=20 and a discrete bound N=10 as input parameters. Because the model has nonlinear polynomial dynamics, we use yices for an underlying solver with the default algorithm 1-step. For the formulas f1, f2, and f3, we choose thresholds ϵ1=1.0, ϵ2=5.0, and ϵ3=4.0, respectively.

STLmc finds counterexamples for f1 and f3, while f2 is safe. The following shows the command finding a counterexample for the STL formula f1:[0,5]((pb40)U[1,8](x<40)) at bound 5 with respect to ϵ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 ϵ |Ψ| Time Result k Alg.
f1 1.0 2.3 3.43 5 1-step
f2 5.0 3.8 0.86 - 1-step
f3 4.0 1.9 2.83 4 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 ϵ=1.0)

Figure [2] shows the visualization graphs generated for f1=[0,5](pb40U[1,8]x<40) with the subformulas: f11=pb40U[1,8]x<40f12=pb40f13=x<40

The robustness degree of f1 is less than ϵ at time 0, since the robustness degrees of f11 is always less than ϵ in the interval [0,5], which is because the degree of f12 is less than ϵ 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