#### High-Level Planning in Robotics

A classical application of reactive synthesis is the domain of automated high-level planning in robotics. We consider a warehouse floor plan with several shelves, see Figure 1. To parametrise the experiment, we consider floor plans with `n * 3` shelves with `2 ≤ n ≤ 20`. A robot operates together among other robots within the warehouse. `TEMPEST` can be used in this setting to synthesize controllers for the robot that perform certain tasks, as well as shields used to ensure safe operation of the robot, or to guarantee performance.

`6 * 3`shelves.

#### Safety-Shield Synthesis

A safety-shield can be synthesized to enforce *collision avoidance* with other robots. In the experiments, we used a finite horizon of `14` steps and a relative threshold of `lambda = 0.9`.

#### Model Specification

We discuss the model given in Figure 2 in detail and describe the different sections of the code. The property used to synthesise the safety shield is given in Figure 3.

The keyword `smg` defines the model to be a *stochastic multiplayer game*.

At first we define the actions controllable by each player with the `player`...`endplayer` struct. Square brackets indicate an *action* to be controlled by the described player.

We then define the grid dimension using an *undefined constant* `w`. Afterwards we define the boundaries for the movement of the two robots as well as the probability of robot `2` getting stuck.

The global variable `move` models the turn-based character of the coalition game. It is toggled between the two players such that they may move in an alternating fashion.

Following this we define multiple formulas to capture the spatial constraints given through the environment. A robot may not move into a shelf given that it is between two shelves. If the two robots are above, or below, a row of shelves they may also not move into the shelf. Lastly we capture whether the robots are moving in a corridor between the rows of shelves.

Next, we label all states for which the robots are on the same field with `crash`.

smg player shieldedRobot [e1], [w1], [n1], [s1] endplayer player adverseryRobot [e2], [w2], [n2], [s2] endplayer // (w+1)x16 - grid //const int w; const int width = 6; const int height = 15; const int xmin = 0; const int xmax = width; const int ymin = 0; const int ymax = height; // probabilty to get stuck const double stuckProp = 1/5; const double notstuckProp = 1 - stuckProp; global move : [0..1] init 0; formula robot1BetweenShelves = !(y1=0 | y1=height); formula robot2BetweenShelves = !(y2=0 | y2=height); formula robot1AboveShelves = mod(x1, 2) = 1; formula robot1BelowShelves = mod(x1, 2) = 1; formula robot2AboveShelves = mod(x2, 2) = 1; formula robot2BelowShelves = mod(x2, 2) = 1; formula robot1OpenRow = mod(y1, 5) = 0; formula robot2OpenRow = mod(y2, 5) = 0; label "crash" = x1=x2 & y1=y2; module robot1 x1 : [0..width] init 0; y1 : [0..height] init ymax; [e1] move=0 & x1<xmax & (!robot1BetweenShelves | robot1OpenRow) -> (x1'=x1+1) & (move'=1); [w1] move=0 & x1>0 & (!robot1BetweenShelves | robot1OpenRow) -> (x1'=x1-1) & (move'=1); [n1] move=0 & y1>0 & !robot1BelowShelves -> (y1'=y1-1) & (move'=1); [s1] move=0 & y1<ymax & !robot1AboveShelves -> (y1'=y1+1) & (move'=1); endmodule module robot2 x2 : [0..width] init xmax; y2 : [0..height] init 0; [e2] move=1 & x2<xmax & (!robot2BetweenShelves | robot2OpenRow) -> notstuckProp : (x2'=x2+1) & (move'=0) + stuckProp : (move'=0); [w2] move=1 & x2>0 & (!robot2BetweenShelves | robot2OpenRow) -> notstuckProp : (x2'=x2-1) & (move'=0) + stuckProp : (move'=0); [n2] move=1 & y2>0 & !robot2BelowShelves -> notstuckProp : (y2'=y2-1) & (move'=0) + stuckProp : (move'=0); [s2] move=1 & y2<ymax & !robot2AboveShelves -> notstuckProp : (y2'=y2+1) & (move'=0) + stuckProp : (move'=0); endmodule

The main part of the modelling is described by the `module` structs. Via these we describe the environment and the movement of the robots. `robot1` (controlled by player `controlledRobot`, see above) starts at position `(0,ymax)`.

The actions available to the robots are modelled as such:

[e1] move=0 & x1<xmax & (!robot1BetweenShelves | robot1OpenRow) -> (x1'=x1+1) & (move'=1);

`[e1]`is the label of the action.`move=0 & x1<xmax & (!robot1BetweenShelves | robot1OpenRow)`is called the*guard*of the action, describing whether this action is enabled or not.`(x1'=x1+1) & (move'=1);`finishes the command by describing the outcome distribution when taking this action.

The robots may move in four directions along the axis, given they current position.

To synthesize a `PreSafety`-shield we define the shielding specification below. The resulting shield file will be called `presafetyk14.shield` as defined in the first angle brackets. We then use the keyword `PreSafety` along with a relative comparison of `0.9` for the shield creation. The coalition which should be shielded consists of the first player and we ask TEMPEST for the allowed actions when assuming to stay safe for the next fourteen time steps.

<presafetyk14, PreSafety, lambda=0.9> <<shieldedRobot>> Pmax=? [ G<=14 !"crash" ];

#### Results

The results for the synthesis times are depicted in Figure 4. The sizes of state space of the game graphs range from `5184` states for `n=2` to `186624` states for `n=20`. The results for optimal-shields use the axis on the right hand-side. To compare our results, we tried to compute a strategy for the optimal controller in `PRISM-games 3.0` which resulted in an error. By proper modelling, we were able to synthesize a safe controller comparable to the safety-shield using `PRISM-games 3.0`, resulting in better synthesis times for `TEMPEST`.

*blue*and

*green*plots.