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.
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.
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" ];
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.