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.
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]((pb≥40)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]((pb≥40)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](pb≥40U[1,8]x<40) with the subformulas: f11=pb≥40U[1,8]x<40f12=pb≥40f13=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