1 Introduction
2 Notation and preliminaries
2.1 Notation
\(\mathbb {N}, \mathbb {Q}, \mathbb {R}\) | Natural, rational & real numbers |
\([N] {:}{=}\{1, \dots , N\} \) | Labeling set of robots |
\([Z] {:}{=}\{1, \dots , Z\} \) | Labeling set of RoI |
\(\mathcal {R} = \bigcup _{z \in [Z]} R_z\) | Union of RoI |
\(\mathcal {W}\) | The workspace of the robots |
L | Lipschitz constant |
\(\mathcal {T}_i\), \(\mathcal {A}_i\), \(\widetilde{\mathcal {T}}_i\) | WTS, TBA, product WTS of robot i |
\((S, S^{\text {init}}, \text {Act}, \longrightarrow , \mathfrak {t}, \varGamma , \mathcal {L})\) | (states, init. states, actions, transition relation, weight, atomic propos., labeling function) |
\((Q, Q^{\text {init}}, \text {CL}, \mathrm{Inv}, E, \text {FS})\) | (states, init. states, clocks, invariance, accepted states) |
\(x_i, v_i, u_i\) | position/orientation, velocity and control input of robot |
\(e_i = x_i - x_{i, d}\) | Error signal to be minimized through DFHOCP |
\(\xi _i = [e_i, v_i]^\top \) | stack vector |
\(f_i, G_i, \delta _i\) | Dynamic model of robot i and disturbance \(\delta _i\) |
\(\mathfrak {e}_i = e_i - \overline{e}_i, \mathfrak {v}_i = v_i - \overline{v}_i\) | Errors between real and nominal signals (state and velocity respectively) |
\(\varOmega _{i,1}, \varOmega _{i,2}\) | Invariant tubes for the errors \(\mathfrak {e}_i\), \(\mathfrak {v}_i\) |
\(P_i, Q_i, R_i\) | Positive definite weight matrices used in DFHOCP |
\(\mathcal {E}_i, \mathcal {V}_i, \mathcal {U}_i, \mathcal {F}_i\) | State constraints, velocity constraints, control input constraints, terminal set of DFHOCP |
T, h | Prediction horizon and constant sampling time period |
\(k_i, \rho _i\) | Tube gains |
\(r^t, w^t\) | Timed run & timed word |
\(\tau (l), l \ge 0\) | Time stamp at position \(l \ge 0\) |
\(\mathcal {M}(x_i, \mathfrak {r}_i)\) | A ball centered at \(x_i\), radius \(\mathfrak {r}_i\) covering robot i |
\(d_i, \mathcal {G}_i(t)\) | Sensing radius & set of neighbors of robot i at time t |
\(\Diamond _I, \square _I, \mathcal {U}_I\) | Eventually, always and until MITL operators |
NMPC | Nonlinear model predictive control |
RoI | Regions of interest |
DFHOCP | Decentralized finite horizon |
Optimal control problem | |
TBA | Timed Büchi automaton |
WTS | Weighted transition system |
MITL | Metric interval temporal logic |
ISS | Input to state stability |
RCI set | Robust control invariant set |
2.2 Nonlinear control
2.3 Nonlinear model predictive control
2.4 Formal verification
-
\(\widetilde{Q} = S \times Q\) is the set of states;
-
\(\widetilde{Q} ^{\text {init}} = S^{\text {init}} \times Q^{\text {init}}\) is the set of initial states;
-
\({\rightsquigarrow }\) is the set of transitions where \((\widetilde{q}, \widetilde{q}') \in {\rightsquigarrow }\) iff:
-
\(\widetilde{q} = (s, q) \in \widetilde{Q} \) and \(\widetilde{q}' = (s', q') \in \widetilde{Q} \),
-
\((s, \cdot , s') \in \longrightarrow \), and
-
there exist \(\mathfrak {g}, \gamma , \text {RS}\) such that \((q, \mathfrak {g}, \text {RS}, \gamma , q') \in E\) where \(\gamma = \mathcal {L}(q')\);
-
-
\(\widetilde{\mathfrak {t}}(q, q') = \mathfrak {t}(s, s')\) if \((q, q') \in \rightsquigarrow \), is a map that assigns a positive weight to each transition;
-
\(\widetilde{F} = \{(s, q) \in \widetilde{Q} : q \in \text {FS}\}\) is a set of accepting states; and
-
\(\widetilde{\mathcal {L}}(s, q) = \mathcal {L}(s)\) is a labeling function.
3 Problem formulation
3.1 System model
3.2 Objectives
3.3 Problem statement
4 Problem solution
4.1 Decentralized feedback control design—part I
4.2 Decentralized feedback control design—part II
4.3 Discrete system abstraction
-
\(S_i = \mathcal {R} = \displaystyle \bigcup \nolimits _{z \in [Z]} \mathcal {R}_z\) is the set of states of the robot that contains all the RoI of the workspace \(\mathcal {W}\);
-
\(S_{i}^{\text {init}} \subseteq S_i\) is a set of initial states defined by the robot’ s initial position \(x_i(0)\) in the workspace;
-
\(\mathrm{Act_i}\) is the set of actions containing the union of all feedback controllers (10) which can navigate the robot i between RoI;
-
\(\longrightarrow _i \subseteq S_i \times \mathrm{Act_i} \times S_i\) is the transition relation. We say that \((\mathcal {R}_{i, s}, u_i, \mathcal {R}_{i, d}) \in \longrightarrow _i\), with \(\mathcal {R}_{i, s}\), \(\mathcal {R}_{i, d} \in \mathcal {R}\) with \(\mathcal {R}_{i, s} \ne \mathcal {R}_{i, d}\) if there exist feedback control law \(u_i \in \mathrm{Act_i}\) as in (10) which can drive the robot from the region \(\mathcal {R}_{i, s}\) to the region \(\mathcal {R}_{i, d}\) without intersecting with any other RoI of the workspace;
-
\(\mathfrak {t}_i\) is the time weight as given in (7) and it is computed by Algorithm 2;
-
\(\mathcal {L}_i\) is the labeling function as given in (6);
-
and \(\varGamma _i\) is the set of atomic propositions imposed by Problem 1.
4.4 Control synthesis
4.5 Complexity analysis
-
C1: the computational complexity of the offline construction of WTS \(\widetilde{\mathcal {T}}_i\) and graph search. In particular, the graph search is performed over the product WTS \(\widetilde{\mathcal {T}}_i\) which has \(|S_i| \cdot |Q_i|\) number of states, i.e., the multiplication between the states of the WTS (number of RoI of the workspace) and the number of states of the TBA. The complexity of the Dijskstra algorithm that is used for the graph search is: \(\mathcal {O} \Big ( |S_i| \cdot |Q_i| + |\text {edges}| \log \big (|S_i| \cdot |Q_i| \big ) \Big )\), where \(|\text {edges}|\) is the number of edges of the product WTS \(\widetilde{\mathcal {T}}_i\).
-
C2: Algorithm 2 is an offline computer simulation and the computational complexity is the same with the complexity of a nominal NMPC algorithm;
-
C3: Algorithm 3 is an offline computer simulation of collision detection which scales with the number of agents;
5 Experimental setup and results
-
the RoI \(\mathcal {R}_z\), \(z \in \{1, 2, 3, 4\}\) depicted with blue color in Fig. 4 which stand for the RoI that the robots are required to visit. The RoI \(\mathcal {R}_z\), \(z \in \{1, 2, 3, 4\}\) map into the atomic propositions that model missions for each robot;
-
the RoI \(\mathcal {R}_5\) depicted with red color in Fig. 4 stands for an unsafe region that the robots should avoid collision with. It holds that \(\mathcal {L}_i(\mathcal {R}_5) = \{ \text {obs} \}\) for every \(i \in [N]\).