A Formal Modular Synthesis Approach for the Coordination of 3-D Robotic Construction with Multi-robots

TL;DR

The paper addresses coordinating multiple robots to construct 3-D structures on a grid using a modular supervisor synthesis framework based on Supervisory Control Theory. It formalizes the problem with automata modeling of both the structure and individual robots, and develops a modular synthesis pipeline that yields local supervisors ($S_i$) which can be replicated across robots. A sufficient condition ensures that nonblocking, task-observer, and totally reciprocal properties of all $S_i$ guarantee a nonblocking, coordinated completion of the target structure. The approach offers a scalable, reactive, permissive control strategy that supports diverse 3-D constructions in decentralized settings, with analyzed computational complexity and demonstrated through an example.

Abstract

In this paper, we deal with the problem of coordinating multiple robots to build 3-D structures. This problem consists of a set of mobile robots that interact with each other in order to autonomously build a predefined 3-D structure. Our approach is based on Supervisory Control Theory, and it allows us to synthesize from models that represent a single robot and the target structure a correct-by-construction reactive controller, called supervisor. When this supervisor is replicated for the other robots, then the target structure can be completed by all robots

Figures (10)

• Figure 1: \ref{['img:3D']} Example of a 3-D structure composed of equal bricks. \ref{['img:2D']} Alternative representation of the 3-D structure in \ref{['img:3D']} by function $h_{{\mathbf{H}_{}}\xspace}$, where each cell $(x , y)$ in two-dimensional grid displays the number of bricks stacked on $(x , y)$. The pair $(0,0)$ represents the region surrounding the construction site. The indexes $x$ and $y$ in $(x , y)$ denote the column and line in the grid, respectively. In this paper, we enumerate the cells according to the convention shown here, that is, indices increase top to bottom and left to right.
• Figure 2: A robot cannot unload a brick in the middle of other bricks.
• Figure 4: $G^{1}$ model to update of the variables $h_{x,y}$. Guard $g_a$ is given by the Boolean-valued function $\exists (x',y') \in \mathcal{N}_{x,y}\xspace \mid h_{x',y'} = h_{x,y}$, whereas $g_b$ is given by $\exists (x',y') , (x",y") \in \mathcal{N}_{x,y}\xspace \mid (h_{x,y} \ge h_{x',y'} \lor h_{x,y} \ge h_{x",y"} ) \land (x' = x" = x \oplus x' = x" = y)$. A transition with whether ${\tau_{i}^{x,y}}\xspace$ or ${\tau_{Other}^{x,y}}\xspace$ can only occur if $g_a \land g_b$ is evaluated to true, and when it occurs, $G^{1}$ changes of state while the value of $h_{x,y}$ is increased by 1.
• Figure 5: Templates for ${G^{}}\xspace_{x,y}^{2}$, with $g_c := h_{x,y} < h_{{\mathbf{H}_{}}\xspace}(x,y) - 1$ and $g_d := h_{x,y} = h_{{\mathbf{H}_{}}\xspace}(x,y) - 1$. Note that, the transition to marked state in ${G^{}}\xspace_{x,y}^2$ is enabled whenever the height at $(x , y)$ is equal to $h_{{\mathbf{H}_{}}\xspace}(i , j)-1$. In this situation, if the robot ${R_{i}}\xspace$ or another robot stack one more brick on $(x,y)$, events ${\tau_{i}^{x,y}}\xspace$ and ${\tau_{Other}^{x,y}}\xspace$, then the target height at $(x,y)$ is achieved and ${G^{}}\xspace_{x,y}^2$ goes to the marked state.
• Figure 6: $G^{3}$ models the navigation and loading of robot $R_{i}$. State ${q}_{0}$ and ${q}_{1}$ have the semantics 'robot outside the grid' and 'robot inside the grid', respectively. State ${q}_{0}$ is chosen to be a marked state. Take, as an example, the transition associated with the event $e_i$ (move east): it can only occur when the robot is on a cell that is not located at the lateral border of the grid (guard $\hat{\mathsf{x}}_{} \xspace< n_x$); upon its occurrence, the $\hat{\mathsf{x}}_{} \xspace$ variable has its value incremented by one (action $\hat{\mathsf{x}}_{} \xspace\coloneqq \hat{\mathsf{x}}_{} \xspace+1$). Guard $g_1$ for the event 'out' is given by the atomic proposition $(\hat{\mathsf{x}}_{} \xspace, \hat{\mathsf{y}}_{} \xspace)\in \mathcal{E}_{}\xspace$.

Theorems & Definitions (2)

• Definition 1
• Theorem 1: MR:WODES2022