Case Studies
This is a variant of the train-gate controller (see e.g., Alur et al.: "Parametric real-time reasoning". In: STOC (1993)) in which a train approaches a crossing, and the controller needs to open and close the gate such that the train can pass. In our case study, the problem is modeled as product of two timed automata, one for the train (left) and one for the gate (right).
The train performs the uncontrollable actions get near, enter, leave, travel in sequence, i.e., approaches and passes through the gate section. The gate may perform the controllable actions start close,start open, finish close, finish open to change its state.
The composed system is declared safe if the gate is closed when the train enters and opens after the train leaves the crossing.
The undesired behavior is given by the MTL-specification
enter Ũ ¬finish close ∨ start open Ũ ¬leave ∨ travel Ũ ¬finish open
Additionally, we have parameterized the problem by the number of crossings and the time it takes the train to reach each crossing. For instance, Railroad(4,8) identifies the problem with two crossings and a duration of 4 and 8 time units before reaching the first, respectively the second crossing.
An exemplary search graph is shown below (only explored nodes are displayed):
The respective controller looks as follows:
A robot transports goods between stations (based on Viehmann et al.: "Transforming robotic plans with timed automata to solve temporal platform constraints". In: IJCAI (2021)). To do so, it can pick and put goods, one at a time. It has a camera that needs to be enabled 1 sec before the robot performs a pick or a put action. As the camera may overheat, it must not run continuously for longer than 4 sec. The camera is controllable with the actions on and off, the robot’s actions pick, put, and move are not controllable. The robot takes exactly 3 sec to move between the stations. The specification of undesired behavior is given as:
¬on U pick ∨ F(off ∧ (¬on U pick )) ∨ F (on U [0,1] pick) ∨ ¬on U put ∨ F(off ∧ (¬on U put)) ∨ F(on U [0,1] put)
A conveyor belt moves luggage in an airport (based on van Hulst et al.: "Maximally permissive controlled system synthesis for non-determinism and modal logic". DEDS 27(1) (2017)). If a piece of luggage gets stuck, the belt must stop, which allows some human operator to remove (release) the stuck luggage. The conveyor must not immediately continue (resume) after stopping but instead wait for at least 2 sec to ensure safety of the operator. Also, the conveyor should not stop without reason. The controllable actions are move and stop, while the uncontrollable actions are release, resume, and stuck. The undesired behavior is specified as follows:
F release ∧ F [0,2] move ∨ (¬stuck ) U stop ∨ F(stop ∧ (¬stuck ) U stop)