Distributed Cooperative Manipulation under Timed Temporal
Specifications
Christos K. Verginis and Dimos V. Dimarogonas
Abstract— This paper addresses the problem of cooperative
manipulation of a single object by N robotic agents under
local goal specifications given as Metric Interval Temporal
Logic (MITL) formulas. In particular, we propose a distributed
model-free control protocol for the trajectory tracking of the co-
operatively manipulated object without necessitating feedback
of the contact forces/torques or inter-agent communication. This
allows us to abstract the motion of the coupled object-agents
system as a finite transition system and, by employing standard
automata-based methodologies, we derive a hybrid control
algorithm for the satisfaction of a given MITL formula. In
addition, we use load sharing coefficients to represent potential
differences in power capabilities among the agents. Finally,
simulation studies verify the validity of the proposed scheme.
I. INTRODUCTION
Multi-agent systems have gained significant attention over
the last decade, since they provide several advantages with
respect to single-agent setups. In the case of object manip-
ulation, complex tasks involving heavy/large payloads and
difficult maneuvers necessitate the employment of more than
one robot. The problem of cooperative manipulation control
has been studied extensively, using centralized schemes,
where a central computer handles the agents’ behavior, as
well as decentralized setups, where each agent determines its
actions on its own, either with partial or no communication
at all [1]–[11].
In contrast to the related literature, which mainly considers
the trajectory tracking of the manipulated object, we would
like to define complex tasks over time, such as "never take
the object to dangerous regions" or "keep moving the object
from region A to B within a predefined time interval" which
must be executed via the control actions of the agents. Such
tasks can be expressed by temporal logic languages, which
can describe complex planning objectives more efficiently
than the well-studied navigation algorithms. Linear Temporal
Logic (LTL) is the most common language that has been
incorporated to the multi-agent motion planning problem
[12]–[16], without however considering time specifications.
Metric and Metric Interval Temporal Logic (MTL, MITL)
[17]–[19] as well as Time Window Temporal Logic (TWTL)
are languages that encode time specifications and were used
for multi-agent motion planning in [20]–[22].
The authors are with the Centre for Autonomous Systems and ACCESS
Linnaeus Centre, KTH Royal Institute of Technology, Stockholm 10044,
Sweden. Emails: {cverginis, dimos}@kth.se.
This work was supported by funding from the Knut and Alice Wallenberg
Foundation, the Swedish Research Council (VR), the European Union’s
Horizon 2020 Research and Innovation Programme under the Grant Agree-
ment No. 644128 (AEROWORKS) and the H2020 ERC Starting Grant
BUCOPHSYS.
Regarding robotic manipulation, high level planning tech-
niques have been proposed in [23]–[25] using common
planning methods like configuration space potential fields
and A∗algorithms. In [25] the motion planning problem for
a group of unicycles manipulating a rigid body is addressed
and in [24] an abstraction methodology is introduced; LTL
specifications are employed in [26], where two mobile robots
transport an object in a leader-follower scheme. Additionally,
temporal logic formulas are utilized in [27] for dexterous
manipulation through robotic fingers and in [28] for single
manipulation tasks, without, however, incorporating the dy-
namics of the robotic arm in the abstracted model. In [29] a
hybrid framework for cooperative manipulation is presented.
For the continuous control part, impedance and/or force
control is the most common methodology [2]–[5], in which
the robotic arms employ sensors to obtain feedback of the
contact forces/torques which, however, may result to perfor-
mance decline due to sensor noise or mounting difficulties.
Moreover, most works in the related literature consider
known dynamic models and/or parameters of the object and
the agents, whose accurate knowledge, however, can be a
challenging issue.
In this paper, we propose a novel hybrid control scheme
for the cooperative manipulation of an object under MITL
specifications. In particular, we develop a distributed model-
free control protocol for the trajectory tracking of the co-
operative manipulated object with prescribed transient and
steady state performance. The latter allows us to abstract
the motion of the coupled system object-agents as a finite
transition system. Then, by employing formal verification-
based methodologies, we derive a path that satisfies a given
MITL task. The control scheme does not use any force/torque
information at the contact points or any inter-agent commu-
nication and incorporates load sharing coefficients to account
for differences in power capabilities among the agents.
The rest of the paper is organized as follows: Section II
introduces notation and preliminary background. Section III
describes the problem formulation and the overall system’s
model. The control strategy is presented in Section IV. Sec-
tion V verifies our approach through numerical simulation
results and Section VI concludes the paper.
II. NOTATION AND PRELIMINARIES
A. Notation
The set of positive integers is denoted as N and the real
n-coordinate space, with n ∈N, as Rn; Rn
≥0 and Rn
>0 are
the sets of real n-vectors with all elements nonnegative and
positive, respectively. Given a set S, 2S is the set of all
arXiv:1610.00913v4  [cs.RO]  6 Feb 2017
subsets of S. The vector connecting the origins of coordinate
frames {A} and {B} expressed in frame {C} coordinates
in 3-D space is denoted as pC
B/A ∈R3. Given a ∈R3,
S(a) is the skew-symmetric matrix defined according to
S(a)b = a × b. The rotation matrix from {A} to {B}
is denoted as RB/A ∈SO(3), where SO(3) is the 3-D
rotation group. The angular velocity of frame {B} with
respect to {A} is denoted as ωB/A ∈R3 and it holds that [30]
˙RB/A = S(ωB/A)RB/A. We further denote as ηA/B ∈T3 the
Euler angles representing the orientation of {B} with respect
to {A} and ωB/A = JB/A(ηB/A) ˙ηB/A; JB/A : T3 →R3×3 is
a smooth function representing the analytic Jacobian and T3
is the 3-D torus. Moreover, B(c, r) denotes the 3-D sphere of
radius r ≥0 and center c ∈R3 and d : R3×R3 →R is the 3-
D Euclidean distance. We further define the set M = R3×T3.
For notational brevity, when a coordinate frame corresponds
to an inertial frame of reference {I}, we will omit its explicit
notation (e.g., pB = pI
B/I, ωB = ωI
B/I, RB = RB/I etc.).
Finally, all vector and matrix differentiations will be with
respect to an inertial frame {I}, unless otherwise stated.
B. Metric Interval Temporal Logic (MITL)
The syntax of MITL over a set of atomic propositions
AP is defined by the grammar φ
:=
p | ¬φ |
⃝I
φ | ♦Iφ | □Iφ | φ1Uφ2, where p ∈AP, ⃝, ♦, □and ∪
are the next, future, always and until operators, respectively.
I is one of the following intervals: [i1, i2], [i1, i2), (i1, i2],
(i1, i2), [i1, ∞), (i1, ∞) with i1, i2 ∈R≥0, i2 > i1.
Given a set of atomic propositions AP, an MITL formula
φ and an infinite sequence r = (r1, t1)(r2, t2) . . . , with rj ∈
2AP and tj ∈R≥0, tj+1 > tj, ∀j ∈N, we define (r, j) |=
φ, j ∈N (r satisfies φ at j) in the point-wise semantics [19]:
(r, j)
|=
p ⇔p ∈rj,
(r, j)
|=
¬φ ⇔(r, j) ̸|= φ
(r, j)
|=
φ1 ∧φ2 ⇔(r, j) |= φ1 and (r, j) |= φ2
(r, j)
|=
⃝Iφ ⇔(r, j + 1) |= φ and tj+1 −tj ∈I
(r, j)
|=
φ1Uφ2 ⇔∃k, j, j ≤k, s.t. (r, k) |= φ2,
tk −tj ∈I and (r, m) |= φ1, ∀j ≤m ≤k.
Also, ♦Iφ = True Uφ and □Iφ = ¬♦I¬φ. The sequence r
satisfies φ, denoted as r |= φ if and only if (r, 1) |= φ. More
information regarding MITL can be found in [18], [19].
C. Dynamical Systems
Consider the initial value problem:
˙ξ = H(t, ξ), ξ(t0) = ξ0 ∈Ωξ,
(1)
with H : [t0, +∞) × Ωξ →Rn where Ωξ ⊂Rn is a non-
empty open set.
Definition 1. [31] A solution ξ(t) of the initial value problem
(1) is maximal if it has no proper right extension that is also
a solution of (1).
Theorem 1. [31] Consider problem (1). Assume that H(t, ξ)
is: a) locally Lipschitz on ξ for almost all t ∈[t0, +∞),
b) piecewise continuous on t for each fixed ξ ∈Ωξ and
c) locally integrable on t for each fixed ξ ∈Ωξ. Then,
Fig. 1.
Two robotic arms rigidly grasping an object.
there exists a maximal solution ξ(t) of (1) on [t0, tmax) with
tmax > t0 such that ξ(t) ∈Ωξ, ∀t ∈[t0, tmax).
Proposition 1. [31] Assume that the hypotheses of Theorem
1 hold. For a maximal solution ξ(t) on the time interval
[t0, tmax) with tmax < ∞and for any compact set Ω′
ξ ⊂Ωξ
there exists a time instant t′ ∈[t0, tmax) such that ξ(t′) /∈
Ω′
ξ.
III. PROBLEM FORMULATION
Consider a bounded workspace W ⊂R3 consisting of
N mobile manipulators rigidly grasping an object, as shown
in Fig. 1. We assume that each agent i ∈{1, . . . , N} has
ni ≥6 degrees of freedom (generalized joint coordinates),
denoted as qi : R≥0 →Rni. We also denote the entire
joint space as q = [qT
1 , · · · , qT
N]T : R≥0 →Rn, with n =
PN
i=1 ni. The reference frames corresponding to the i-th end-
effector and the object’s center of mass are denoted with
{Ei} and {O}, respectively, whereas {I} corresponds to an
inertial reference frame. The rigidity of the grasps implies
that the agents can exert any forces/torques along every
direction to the object. We consider that each agent i knows
the position and velocity only of its own joint variables qi
as well as its own and the object’s geometric parameters.
Moreover, no interaction force/torque measurements or on-
line communication is required and the dynamic model of
the object and the agents is considered unknown. Finally,
we assume that the robotic agents and the object are away
from kinematic and representation singularities [30].
A. System model
1) Kinematics: In view of Fig. 1, we have that
pEi(q)
=
pO(q) + pEi/O(q) = pO(q) + REi(q)p
Ei
Ei/O
ηEi(q)
=
ηO(q) + αi,
(2)
where αi ∈T3 is a known angular offset. We further define
xEi, xO : Rn →M with xEi(q) = [pT
Ei(q), ηT
Ei(q)]T and
xO(q) = [pT
O(q), ηT
O(q)]T . Note that, since (2) holds for all
i ∈{1, . . . , N}, the physical coupling between the object
and the agents creates a dependence of xO and xEi on all
q. Moreover, the grasp rigidity implies that ωEi = ωO, i.e.,
JEi(ηEi(q)) ˙ηEi = JO(ηO(q)) ˙ηO. Since the agents and the
object are away from representation singularities, J−1
O
and
J−1
Ei are well-defined and smooth and hence we differentiate
(2) to obtain:
˙xEi = JOi(xEi, xO) ˙xO,
(3)
where JOi : M×M →R6×6 is the Jacobian from the object
to the i-th agent:
JOi =
 I3×3
S(pO/Ei)JO(ηO)
03×3
J−1
Ei (ηEi)JO(ηO)

,
(4)
which is always invertible due to the grasp rigidity.
Furthermore,
by
noticing
that
REi(q)p
Ei
Ei/O
=
RO(ηO)pO
Ei/O, (2) can be rewritten as
xEi = fOi(xO),
(5)
where fOi : M →M represents the coupled kinematics.
Remark 1. Each agent i can compute xEi, ˙xEi via its
forward and differential kinematics [30] xEi = ki(qi) and
˙xEi = Ji(qi) ˙qi, respectively, where ki : Rni →R3 and
Ji(qi) = ∂ki(qi)/∂qi is the corresponding Jacobian. In
addition, since the geometric parameters p
Ei
Ei/O and αi are
known, xO and ˙xO can be computed by inverting eq. (2) and
(3), without employing any sensory data.
2) Object Dynamics : The Newton-Euler equation for
the object’s second order dynamics is:
MO(xO)¨xO + CO(xO, ˙xO) ˙xO + gO(xO) + wO(t) = λO,
(6)
where MO : M →R6×6 is the positive definite inertia
matrix, CO : M × R6 →R6×6 is the Coriolis matrix,
gO : M →R6 is the gravity vector, wO : R≥0 →R6 is
a bounded vector representing external disturbances and λO
is the force vector acting on the object’s center of mass. All
aforementioned vector fields are continuous and unknown.
3) Agent Dynamics : The task-space dynamics for agent
i ∈{1, . . . , N} are given by [30]:
Mi(xEi)¨xEi + Ci(xEi, ˙xEi) ˙xEi + gi(xEi)
+fi(xEi, ˙xEi) + wi(t) + λi
=
ui
(7)
where Mi : M →R6×6 is the task-space positive definite
inertia matrix, Ci : M × R6 →R6 represents the task-
space Coriolis matrix, gi : M →R6 is the task-space
gravity vector, fi
: M × R6
→R6 is a vector field
representing model uncertainties and wi : R≥0 →R6 is a
bounded vector representing external disturbances. Similarly
to (6), the aforementioned vector fields are continuous and
completely unknown; ui ∈R6 is the task space wrench
acting as the control input and λi ∈R6 is the generalized
force vector that agent i exerts on the object.
Remark 2. The task-space wrench ui can be translated to
the joint space inputs τi ∈Rni via τi = JT
i (qi)ui+(Ini×ni−
JT
i (qi) ¯JT
i (qi))τi0, where ¯Ji is a generalized inverse of Ji
[30]. The term τi0 concerns redundant agents (ni > 6) and
does not contribute to end-effector forces.
4) Coupled Dynamics : The kineto-statics duality [30]
along with the grasp rigidity suggest that the force λO acting
on the object center of mass and the generalized forces
λi, i ∈{1, . . . , N} exerted by the agents at the contact points
are related through
λO = GT (x)λ,
(8)
(a) Illustration of ˆL
(b) Workspace Discretization
Fig. 2.
(a): An example of the agents of Fig. 1 in the configuration that
derives ˆL. (b): The workspace partition according to the bounding box of
the coupled system.
where x = [xT
O, xT
E]T ∈MN+1, xE = [xT
E1, · · · , xT
EN ]T ∈
MN, λ = [λT
1 , · · · , λT
N]T ∈R6N and G : MN+1 →R6N×6
is the grasp matrix, with G(x) = [JT
O1, · · · , JT
ON ]T .
Next, we substitute (3) and its derivative in (7) and we
obtain in vector form after rearranging terms:
λ
=
u −M(xE)G(x)¨xO −g(xE) −f(xE) −w(t)
−(M(xE) ˙G(x, ˙x) + C(xE, ˙xE)G(x)) ˙xO
(9)
where
we
have
used
the
stack
forms
M
=
diag{[Mi]i∈{1,...,N}}, C
=
diag{[Ci]i∈{1,...,N}}, g
=
[gT
1 , · · · , gT
N]T , f
= [f T
1 , · · · , f T
N]T , u = [uT
1 , · · · , uT
N]T
and w = [wT
1 , · · · , wT
N]T . By substituting (9) and (6) in (8),
we obtain the coupled dynamics:
f
M(x)¨xO + eC(x, ˙x) ˙xO +eh(x, ˙x)+ ew(x, t) = GT (x)u, (10)
where f
M(x) = MO + GT MG, eC(x, ˙x) = CO + GT M ˙G +
GT CG,eh(x, ˙x) = gO + GT g + GT f, and ew(x, t) = wO +
GT w. It is straightforward to deduce the positive definiteness
of f
M as well as the continuity of all the above coupled vector
fields due to the continuity of the individual terms.
B. Workspace Partition
As mentioned in Section I, we are interested in defining
MITL formulas over certain properties in a discrete set of
regions of the workspace. Therefore, we provide now a
partition of W into cell regions. We first define the set Sq
that consists of all points ps ∈W that physically belong
to the coupled system, i.e. they consist part of either the
agents’ or the object’ volume. Note that these points depend
directly on the actual value of q. We further define the
constant ˆL ≥sup q∈Rn
ps∈Sq
d(ps, pO(q)). Note that, although the
explicit computation of Sq may not be possible, ˆL is an upper
bound of the maximum distance between the object center
of mass and a point in the coupled system’s volume over all
possible configurations q, and thus, it can be measured. For
instance, Fig. 2(a) shows ˆL for the system of Fig. 1. It is
straightforward to conclude that
ps ∈B(pO(q), ˆL), ∀ps ∈Sq, q ∈Rn.
(11)
Next, we partition the workspace W into R equally sized
rectangular regions Π = {π1, . . . , πR}, whose geometric
centers are denoted as pc
πj ∈W, j ∈{1, . . . , R}. The length
of the region sides is set as D = 2ˆL + 2l0, where l0 is
an arbitrary positive constant. Hence, each region πj can be
formally defined as follows:
πj
=
{p ∈W s.t. (p)k ∈[(pc
πj)k −ˆL −l0, (pc
πj)k + ˆL + l0),
∀k ∈{x, y, z}},
with d(pc
πj+1, pc
πj) = (2ˆL + 2l0), ∀j ∈{1, . . . , R −1}
and (pc
πj)z
=
ˆL + l0, ∀j
∈{1, . . . , R}. The notation
(a)k, k ∈{x, y, z} denotes the k-th coordinate of a =
[(a)x, (a)y, (a)z]T ∈R3. An illustration of the aforemen-
tioned partition is depicted in 2(b).
Note that each πj is a uniformly bounded, convex and
well-connected set and also πj ∩πj′ = ∅, ∀j, j′ ∈{1, . . . , R}
with j ̸= j′. We also define the neighborhood of region
πj as the set of its adjacent regions D(πj) = {πj′ ∈
Π s.t. d(pc
πj, pc
πj′ ) = (2ˆL + 2l0)}, which is symmetric, i.e.,
πj′ ∈D(πj) ⇔πj ∈D(πj′).
To proceed we need the following definitions regarding the
timed transition of the coupled system between two regions
πj, πj′:
Definition 2. The coupled system object-agents is in region
πj at a configuration q, denoted as A(q) ∈πj, if and only
if (i) ps ∈πj, ∀ps ∈Sq and (ii) d(pO(q), pc
πj) < l0.
Definition 3. Assume that A(q(t0)) ∈πj, j ∈{1, . . . , R},
for some t0 ∈R≥0. Then, there exists a transition for the
coupled system object-agents from πj to πj′, j′ ∈{1, . . . , R}
with time duration δtj,j′ ∈R≥0, denoted as πj →πj′, if and
only if there exists a bounded control trajectory u in (10),
such that A(q(t0 + δtj,j′)) ∈πj′ and ps ∈πj ∪πj′, ∀ps ∈
Sq, t ∈[t0, t0 + δtj,j′].
Note that the entire system object-agents must remain in
πj, πj′ during the transition and therefore the requirement
πj′ ∈D(πj) is implicit in the definition above.
C. Specification
Given the workspace partition, we can introduce a set of
atomic propositions AP for the object, which are expressed
as boolean variables that correspond to properties of interest
in the regions of the workspace (e.g., "Obstacle region",
"Goal region"). Formally, the labeling function L : Π →
2AP assigns to each region πj the subset of the atomic
propositions AP that are true in πj.
Definition 4. Assume that q(t) is a trajectory. Then,
a timed sequence of q is the infinite sequence β
=
(q1(t), t1, )(q2(t), t2, ) . . . , with tm ∈R≥0, tm+1 > tm
and A(qm(tm))
∈
πjm, jm
∈
{1, . . . , R}, ∀m
∈
N.
The timed behavior of β is the infinite sequence σβ =
(σ1, t1)(σ2, t2) . . . , with σm ∈2AP, σm ∈L(πjm) for
A(qm(tm)) ∈πjm, jm ∈{1, . . . , R}, ∀m ∈N, i.e., the set of
atomic propositions that are true when A(qm(tm)) ∈πjm.
Definition 5. The timed run β satisfies an MITL formula φ
if and only if σβ |= φ.
Fig. 3.
A transition between two adjacent regions πj and πj′. Since
pO ∈B(pd(t), l0), we conclude that ps ∈B(pO, ˆL) ∈B(pd(t), l0+ ˆL) ∈
πj ∪πj′ .
We are now ready to state the problem treated in this paper.
Problem 1. Given N agents rigidly grasping an object
in W subject to the coupled dynamics described by (10),
the workspace partition Π such that A(q(0)) ∈πj, j ∈
{1, . . . , R}, a MITL formula φ over AP and the labeling
function L, develop a control strategy that achieves a timed
sequence β which yields the satisfaction of φ.
IV. MAIN RESULTS
A. Control Design
The first ingredient of the proposed solution, which con-
stitutes one of the main novelties of this work, is the design
of a decentralized control protocol u such that a transition
relation between two adjacent regions according to Def. 3
is established. Assume, therefore, that A(q(t0)) ∈πj, t0 ∈
R≥0. We wish to find a bounded u, such that (i) A(q(t0 +
δtj,j′)) ∈πj′ with πj′ ∈D(πj) and (ii) ps ∈πj ∪πj′, ∀ps ∈
Sq, t ∈[t0, t0 + δtj,j′], for a predefined arbitrary constant
δtj,j′ ∈R≥0 corresponding to the transition πj →πj′.
The first step is to associate to the transition a smooth
trajectory defined by the line segment that connects pc
πj and
pc
πj′ , i.e. define pd : [t0, ∞) →R3, such that pd(t0) =
pc
πj, pd(t) = pc
πj′ , ∀t ≥t0 + δtj,j′ and
B(pd(t), ˆL + l0) ∈πj ∪πj′, ∀t ≥t0.
(12)
If we guarantee that the object’s center of mass stays l0-
close to pd, i.e., d(pO(t), pd(t)) < l0, then d(pO(t0 +
δtj,j′), pc
πj′ ) < l0 and, by invoking (11) and (12), we obtain
ps ∈B(pO(t), ˆL) ∈B(pd(t), ˆL + l0) ∈πj ∪πj′, ∀ps ∈
Sq, t ≥t0 (and therefore t ∈[t0, t0 + δtj,j′]), and thus the
requirements of Def. 3 for the transition relation are met. Fig.
3 illustrates the aforementioned reasoning. Along with pd, we
also define a desired smooth trajectory ηd : [t0, ∞) →T3 for
the object orientation and we form the desired pose trajectory
xd : [t0, ∞) →M, with xd(t) = [xd1(t), . . . , xd6(t)]T =
[pT
d (t), ηT
d (t)]T . We can now define the associated pose
errors es : [t0, ∞) →M with
es(t) = [es1(t), · · · , es6(t)]T = xO(q(t)) −xd(t).
(13)
A suitable methodology for the control design in hand is that
of prescribed performance control, recently proposed in [32],
which is adapted in this work in order to achieve predefined
transient and steady state response bounds for the pose errors.
As stated in [32], prescribed performance characterizes the
behavior where the aforementioned errors evolve strictly
within a predefined region that is bounded by absolutely
decaying functions of time, called performance functions.
The mathematical expressions of prescribed performance are
given by the inequalities: −ρsk(t) < esk(t) < ρsk(t), ∀k ∈
{1, . . . , 6}, where ρsk : [t0, ∞) →R>0 with ρsk(t) =
(ρ0
sk −ρ∞
sk)e−lsk (t−t0) +ρ∞
sk and lsk > 0, ρ0
sk > ρ∞
sk > 0, are
designer-specified, smooth, bounded and decreasing positive
functions of time with positive parameters lsk, ρ∞
sk, incor-
porating the desired transient and steady state performance
respectively. In particular, the decreasing rate of ρsk, which
is affected by the constant lsk, introduces a lower bound
on the speed of convergence of esk(t). Furthermore, the
constants ρ∞
sk can be set arbitrarily small, achieving thus
practical convergence of the pose errors to zero.
Next, we propose a state feedback control protocol that
does not incorporate any information on the agents’ or the
object’s dynamics or the external disturbances and guarantees
that |esk(t)| < ρsk(t) for all [t0, ∞) and hence [t0, t0 +
δtj,j′], which, by appropriately selecting ρsk(t) and given
that A(q(t0)) ∈πj, guarantees a transition πj →πj′ with
time duration of δtj,j′. Thus, given the pose errors (13):
Step I-a. Select the corresponding functions ρsk(t) =
(ρ0
sk −ρ∞
sk)e−lsk )(t−t0) + ρ∞
sk
with ρ0
sk
=
l0, ∀k
∈
{1, 2, 3}, ρ0
sk > |esk(t0)|, ∀k ∈{4, 5, 6} and ρ0
sk > ρ∞
sk >
0, lsk > 0, ∀k ∈{1, . . . , 6}.
Step I-b. Define the normalized errors ξsk : [t0, ∞) →R:
ξsk(t) = ρ−1
sk (t)esk(t), ∀k ∈{1, . . . , 6},
(14)
and design the reference velocity vector as ˙x∗
d : R6 ×
[t0, ∞) →R6, with ˙x∗
d = [ ˙x∗
d1, . . . , ˙x∗
d6]T and:
˙x∗
dk(ξsk, t) = −gskεsk(ξsk), ∀k ∈{1, . . . , 6},
(15)
where gsk > 0 and εsk : R →R is the transformed error:
εsk(ξsk) = ln
1 + ξsk
1 −ξsk

, ∀k ∈{1, . . . , 6}.
(16)
Before proceeding, note that (13) and (14) suggest that
xO
= Ps(t)ξs + xd(t), where ξs
= [ξs1, . . . , ξs6]T and
Ps = diag{[ρsk]k∈{1,...,6}} . Therefore, by employing (5) we
can write x = [xT
O, f T
O1(xO), . . . , f T
ON (xO)]T = [ξT
s Ps(t) +
xT
d (t), f T
O1(Ps(t)ξs + xd(t)), . . . , f T
ON (Ps(t)ξs + xd(t))]T
=
f O(Ps(t)ξs +xd(t)), i.e., we can express x as a function of ξs
and t. Therefore, in the following, the dependence on x will
directly imply dependence on ξs, t. Similarly, dependence on
˙x will imply dependence on ξs, ˙ξs and t.
Step
II-a.
Define
the
velocity
error
vector
ev
:
R6 × [t0, ∞)
→
R6
with
ev(ξs, t)
=
[ev1(ξs1, t), . . . , ev6(ξs6, t)]T
=
˙xO(q(t)) −
˙x∗
d(ξs, t)
and
select
the
corresponding
positive
performance
functions ρvk : [t0, ∞) →R>0 with ρvk(t) = (ρ0
vk −
ρ∞
vk)e−lvk (t−t0) + ρ∞
vk, such that ρ0
vk > |evk(t0)|, lvk > 0
and ρ0
vk > ρ∞
vk > 0, ∀k ∈{1, . . . , 6}.
Step II-b. Define the normalized velocity errors ξv :
[t0, ∞) →R6:
ξv(t) = [ξv1(t), . . . , ξv6(t))]T = P −1
v
(t)ev(ξs(t), t),
(17)
where Pv(t) = diag{[ρvk(t)]k∈{1,...,6}}, and design the
distributed control protocol ui : R6 × R6 × [t0, ∞) →R6:
ui(ξs, ξv, t) = −cigvJ−T
Oi (x)P −1
v
(t)Rv(ξv)εv(ξv),
(18)
where gv > 0, JOi as defined in (4) and ci are predefined
load sharing coefficients satisfying P
i∈{1,...,N} ci = 1 and
0 ≤ci ≤1, ∀i ∈{1, . . . , N}. Also, Rv : R6 →R6×6, εv :
R6 →R6 are defined as:
Rv(ξv)
=
diag
n
2(1 −ξ2
vk)−1
k∈{1,...,6}
o
(19)
εv(ξv)
=

ln
1 + ξv1
1 −ξv1

, . . . , ln
1 + ξv6
1 −ξv6
T
(20)
The control law (18) can be written in vector form u =
[uT
1 , . . . , uT
N]T :
u(ξs, ξv, t) = U j′
j (t) = −CgG∗(x)P −1
v
(t)Rv(ξv)εv(ξv),
(21)
where Cg = gvdiag{[ciI6×6]i∈{1,...,N}} ∈R6N×6N
≥0
, G∗(x) =
[J−1
O1 , . . . , J−1
ON ]T ∈R6N×6 and the notation U j′
j
stands for
the transition from πj to πj′.
Remark 3. It can be verified by (15) and (18) that the
proposed control protocol is distributed in the sense that
each agent needs feedback only from the state of the ob-
ject’s center of mass, which can be obtained by (2) and
(3), as discussed in Section III-A. The parameters needed
for the computation of ρsk, ρvk, ηd as well as gsk, ci, k ∈
{1, . . . , 6}, i ∈{1, . . . , N} can be transmitted off-line to
the agents. Moreover, the overall control scheme does not
incorporate any prior knowledge of the model nonlineari-
ties/disturbances or force/torque measurements at the contact
points.
Remark 4. Note that internal force regulation can be
also guaranteed by including in (21) a term of the form
(I6N −1
N G∗GT ) ˆfint,d, where ˆfint,d is a constant vector that
can be transmitted off-line to the agents. Nevertheless, the
computation of G∗GT requires knowledge of all grasping
points pEi, which reduces to knowledge of the offsets pO
Ei/O
(since the agents can compute RO and pO), that can be also
transmitted off-line to the agents.
The next theorem summarizes the results of this section.
Theorem 2. Consider N agents rigidly grasping an object
with unknown coupling dynamics described by (10) and
A(q(t0)) ∈πj, j ∈{1, . . . , R}. Then, the distributed control
protocol (14)-(20) guarantees that πj →πj′ with time
duration δtj,j′ and all closed loop signals being bounded,
and thus establishes a transition relation between πj and πj′
for the coupled system object-agents, according to Def. 3.
Proof. Differentiating (14) and (17) with respect to time,
employing (13), (10) as well as the facts that ˙xO = ˙x∗
d +
Pv(t)ξv, PN
i=1 ci = 1 and substituting (15), (21), we obtain:
˙ξsk(ξ, t)
=
hsk(ξ, t)
=
−gskρ−1
sk (t)εsk(ξsk) −ρ−1
sk (t)( ˙xdk(t)
+ ˙ρsk(t)ξsk −ρvk(t)ξvk), ∀k ∈{1, . . . , 6} (22)
˙ξv(ξ, t)
=
hv(ξ, t)
=
−gvP −1
v
(t)f
M −1(x)P −1
v
(t)Rv(ξv)εv(ξv)
−P −1
v
(t)
h
f
M −1(x)( eC(x, ˙x)(Pv(t)ξv + ˙x∗
d)
+eh(x, ˙x) + ew(x, t)) + ˙Pv(t)ξv + ∂
∂t ˙x∗
d

(23)
for all t ≥t0 with ξ(t) = [ξT
s (t), ξT
v (t)]T . By defining h :
R6×R6×[t0, ∞) →R12, we can write (22), (23) in compact
form:
˙ξ = h(ξ, t) = [hT
s (ξ, t), hT
v (ξ, t)]T
(24)
We further define the open and nonempty set Ωξ = Ωξs ×
Ωξv ⊂R12 with Ωξs = Ωξv = (−1, 1)6.
Since
A(q(t0))
∈
πj,
Def.
2
implies
that
d(pO(q(t0)), pc
πj)
<
l0.
Also,
pd(t0)
=
pc
πj.
Therefore,
by
choosing
ρ0
sk
=
l0, ∀k
∈
{1, 2, 3}
as
well
as
ρ0
sk
>
|esk(t0)|, ∀k
∈
{4, 5, 6}
we
guarantee that ξs(t0) ∈Ωξs. Furthermore, by selecting
ρ0
vk
>
|evk(t0)|, ∀k
∈
{1, . . . , 6}, we guarantee that
ξv(t0)
∈
Ωξv. Thus, we conclude that ξ(t0)
∈
Ωξ.
Additionally, h is continuous on t and locally Lipschitz on
ξ over Ωξ. Therefore, according to Theorem 1, there exists
a maximal solution ξ(t) of (24) on a time interval [t0, tmax)
such that ξ(t) ∈Ωξ, ∀t ∈[t0, tmax). Thus:
ξmk(t) = emk
ρmk
∈(−1, 1), ∀k ∈{1, . . . , 6}, m ∈{s, v}
(25)
∀t ∈[t0, tmax), from which we obtain that esk(t) and evk(t)
are bounded by ρsk(t) and ρvk(t), respectively. Therefore,
the error vectors εsk(ξs), ∀k ∈{1, . . . , 6} and εv(ξv), as
defined in (16) and (20), respectively, are well defined for
all t ∈[t0, tmax). Hence, consider the positive definite
and radially unbounded functions Vsk : R →R≥0 with
Vsk(εsk) = ε2
sk, ∀k ∈{1, . . . , 6}. By differentiating Vsk with
respect to time and substituting (22), we obtain:
˙Vsk = −4εskρ−1
sk (t)
1 −ξ2sk
(gskεsk + ˙xdk(t) + ˙ρsk(t)ξsk −ρvk(t)ξvk)
Next, since ˙xdk, ρvk, ˙ρsk are bounded by construction and
ξsk, ξvk are bounded in (−1, 1) owing to (25), ˙Vsk becomes:
˙Vsk ≤4ρ−1
sk (t)
1 −ξ2sk
(Bs|εsk| −gsk|εsk|2),
∀t ∈[t0, tmax), where Bs is an unknown positive constant
independent of tmax satisfying Bs ≥| ˙xdk(t) + ˙ρsk(t)ξsk −
ρvk(t)ξvk| . Therefore, we conclude that ˙Vsk is negative when
|εsk| > Bsg−1
sk and subsequently that
|εsk(ξsk(t))| ≤εsk = max

|εsk(ξsk(t0))|, Bsg−1
sk
	
, (26)
∀t ∈[t0, tmax), k ∈{1, . . . , 6}. Furthermore, from (16),
taking the inverse logarithm, we obtain:
−1 < e−εsk −1
e−εsk + 1 = ξsk ≤ξsk(t) ≤ξsk = eεsk −1
eεsk + 1 < 1 (27)
∀t ∈[t0, tmax), k ∈{1, . . . , 6}. Due to (26), the reference
velocity vector ˙x∗
d(ξs, t), as defined in (15), remains bounded
for all t ∈[t0, tmax). Moreover, invoking ˙xO = ˙x∗
d(ξs, t) +
Pv(t)ξv and (25), we also conclude the boundedness of
˙xO for all t ∈[t0, tmax). Finally, differentiating ˙x∗
d(ξs, t)
with respect to time and employing (22), (25) and (27), we
conclude the boundedness of ∂
∂t ˙x∗
d(ξs, ˙ξs, t), ∀t ∈[t0, tmax).
Applying the aforementioned line of proof, we consider
the positive definite and radially unbounded function Vv :
R6 →R with Vv(εv) = 0.5∥εv∥2. By differentiating Vv
with respect to time, we substitute (23) and by employing
(i) the continuity of f
M, eC,eh and (ii) the boundedness of
wO, wi, ξs, ξv, ˙Pv, ∂
∂t ˙x∗
d, ∀t ∈[t0, tmax), we obtain:
˙Vv ≤∥P −1
v
(t)Rv(ξv)εv∥(Bv −gvλm∥P −1
v
(t)Rv(ξv)εv∥)
∀t ∈[t0, tmax), where λm is the minimum singular value
of the positive definite matrix f
M −1 and Bv is a positive
constant independent of tmax, satisfying
Bv
≥



f
M −1(x)(C(x, ˙x)(Pv(t)ξv + ˙x∗
d(t)) + eh(x, ˙x)+
ew(x, t) + ˙Pvξv + ∂
∂t ˙x∗
d(ξs, ˙ξs, t))




Therefore,
˙Vv
is
negative
when
∥P −1
v
(t)Rv(ξv)εv∥
>
Bv(gvλm)−1, which, by employing the definitions of Pv
and Rv, becomes ∥εv∥> Bv(gvλm)−1ρ0
vk, with ρ0
vk
=
maxk∈{1,...,6}{ρ0
vk}. Therefore, we conclude that
∥εv(ξv(t))∥≤εv = max

εv(ξv(t0)), Bv(gvλm)−1ρ
0
vk
	
,
∀t ∈[t0, tmax). Furthermore, from (20), taking the inverse
logarithm and invoking that |εvk| ≤∥εv∥, we obtain:
−1 < e−εvk −1
e−εvk + 1 = ξvk ≤ξvk(t) ≤ξvk = eεvk −1
eεvk + 1 < 1 (28)
∀t ∈[t0, tmax), k ∈{1, . . . , 6}, which also leads to the
boundedness of the distributed control protocol (21). Up to
this point, what remains to be shown is that tmax can be
extended to ∞. In this direction, notice by (27) and (28)
that ξ(t) ∈Ω′
ξ = Ω′
ξs × Ω′
ξv, ∀t ∈[t0, tmax), where:
Ω′
ξm = [ξm1, ξm1] × · · · × [ξm6, ξm6], m ∈{s, v}
are nonempty and compact subsets of Ωξs and Ωξv, respec-
tively. Hence, assuming that tmax < ∞and since Ω′
ξ ⊂Ωξ,
Proposition 1 dictates the existence of a time instant t′ ∈
[t0, tmax) such that ξ(t′) /∈Ω′
ξ, which is a clear contradiction.
Therefore, tmax = ∞. Thus, all closed loop signals remain
bounded and moreover ξ(t) ∈Ω′
ξ, ∀t ≥t0.
By multiplying (27) with ρsk(t), we obtain |esk(t)| <
ρsk(t), ∀k ∈{1, . . . , 6} and hence |esk(t)| < l0, ∀k ∈
{1, 2, 3}, t ∈[t0, ∞), since ρ0
sk = l0, ∀k ∈{1, 2, 3}. There-
fore, pO(q(t)) ∈B(pd(t), l0), ∀t ≥t0 and, consequently,
pO(q(t0 + δtj,j′)) ∈B(pc
πj′ , l0), since pd(t0 + δtj,j′) =
pc
πj′ . Also, since pO(q(t)) ∈B(pd(t), l0), we deduce that
B(pO(q(t)), ˆL) ∈B(pd(t), l0 + ˆL) and invoking (11) and
(12), we conclude that ps ∈πj ∪πj′, ∀t ∈[t0, t0 + δtj,j′] ⊂
[t0, ∞), and therefore a transition relation with time duration
δtj,j′ is successfully established.
Remark 5. Instead of employing the control protocol (21)
over [t0, ∞), we can define it over a finite time interval as
u = U j′
j ([t0, t0 +δtj,j′)). In that case, it follows by the con-
tinuity of d, pO, pd that limt→(t0+δtj,j′)−d(pO(t), pd(t)) =
d(pO(t0+δtj,j′), pc
πj′ ) and therefore, the transition πj →πj′
with time duration δtj,j′ is still achieved. Moreover, the
predefined selection of δtj,j′ for each transition πj →πj′ is
related to the control capabilities of the agents, since smaller
δtj, j′ will produce larger, but still bounded, ˙x∗
d and u.
B. High-Level Plan Generation
The second part of our solution is the derivation of a high-
level plan that satisfies the given MITL formula φ and can
be generated using standard techniques from automata-based
formal verification methodologies. Thanks to our proposed
control law that allows the transition πj →πj′ for all
πj ∈Π with πj′ ∈D(πj) in a predefined time interval
δtj,j′, we can abstract the motion of the coupled system
object-agents as a finite weighted transition system (WTS)
[33] T = {Π, Π0, →, AP, L, γ}, where Π is the set of states
defined in Section III-B, Π0 ⊂Π is a set of initial states,
→⊆Π × Π is a transition relation according to Def. 3, AP
and L are the atomic propositions and the labeling function,
respectively, as defined in Section III-C, and γ :→→R≥0 is
a map that assigns to each transition its time duration, i.e.,
γ(πj →πj′) = δtj,j′. Therefore, by designing the switching
control protocol U rj+1
rj
(t) from (21):
u = U rj+1
rj
(t), ∀t ∈[tj, tj + δtrj,rj+1), j ∈N,
(29)
with (i) t1
= 0, (ii) tj+1
= tj + δtrj,rj+1 and (iii)
rj ∈{1, . . . , R}, ∀j ∈N, we can define a timed run of
the WTS as an infinite sequence r = (πr1, t1)(πr2, t2) . . . ,
where πr1 ∈Π0 with A(q(0)) ∈πr1, πrj
∈Π, rj ∈
{1, . . . , R} and tj are the corresponding time stamps such
that A(q(tj)) ∈πrj, ∀j ∈N. Every timed run r generates
a timed word w(r) = (L(πr1), t1)(L(πr2), t2) . . . over AP
where L(πrj), j ∈N is the subset of the atomic propositions
AP that are true when A(q(tj)) ∈πrj.
The given MITL formula φ is translated into a Timed Büchi
Automaton At
φ [17] and the product Ap = T ⊗At
φ is built
[33]. The projection of the accepting runs of Ap onto T
provides a timed run rφ of T that satisfies φ; rφ has the
form rφ = (πr1, t1)(πr2, t2) . . . , i.e., an infinite1 sequence
of regions πrj to be visited at specific time instants tj (i.e.,
A(q(tj)) ∈πrj) with t1 = 0 and tj+1 = tj + δtrj,rj+1, rj ∈
{1, . . . , R}, ∀j ∈N. More details on the technique are
beyond the scope of this paper and the reader is referred
to [17], [20], [33].
The execution of rφ = (πr1, t1)(πr2, t2) . . . produces
a trajectory q(t), t ∈R≥0, with timed sequence βφ =
(q1(t), t1)(q2(t), t2) . . . , with A(qj(tj)) ∈πrj, ∀j ∈N.
Following Def. 4, βφ has the timed behavior σβφ
=
(σ1, t1)(σ2, t2) . . . with σj
∈L(πrj), for A(qj(tj)) ∈
1It can be proven that if such a run exists, then there also exists a run that
can be always represented as a finite prefix followed by infinite repetitions
of a finite suffix [33].
(a) A robotic agent
(b) Top view of the initial workspace
Fig. 4.
(a): A robotic agent. (b): Top view of the initial workspace with
three agents (with blue, red and green) carrying an object (with black) in
π1. Goal regions are marked with blue and green whereas obstacle regions
with red.
πrj, ∀j ∈N. Since all πrj belong to rφ, ∀j ∈N, the latter
implies that σβφ |= φ and therefore that βφ satisfies φ. The
aforementioned discussion is summarized as follows:
Theorem 3. The execution of rφ = (πr1, t1)(πr2, t2) . . . of
T that satisfies φ guarantees a timed behavior σβφ of the
coupled system object-agents that yields the satisfaction of
φ and provides, therefore, a solution to Problem 1.
V. SIMULATION RESULTS
The validity of the proposed framework is verified through
simulation studies. We consider three robots consisting of
two joints, three links and a mobile platform that is able
to move along the x −y plane (Fig. 4(a)). We denote as
qi = [pT
c,i, ηT
c,i, qi1, qi2]T ∈R8 the generalized coordinates
of each agent, where pc,i, ηc,i ∈R3 denote the position and
orientation of the ith agent’s platform and qi1, qi2 are the
joint angles, ∀i ∈{1, 2, 3}. The agents grasp a rigid rod of
length 0.4m. The initial coordinates of the system are taken
as pc,1(0) = [1.06, 2, 0.1]T m, pc,2(0) = [2.14, 2, 0.1]T m,
pc,3(0) = [1.6, 2.34, 0.1]T m, ηc,1(0) = [0, 0, 0]T r, ηc,2(0) =
[0, 0, π]T r, ηc,3(0) = [0, 0, −π/2]T r, qi1 = qi2 = π
4 r, ∀i ∈
{1, 2, 3}, and pO(0) = [1.6, 2, 0.44]T m, ηO(0) = [0, 0, 0]T r.
The workspace is partitioned into R = 16 regions, with
ˆL = 1.5m, l0 = 0.5m and pc
π1 = [2, 2, 2]T m, from which
it can be verified that A(q(0)) ∈π1. We further choose
δtj,j′ = 5s, ∀j, j′ ∈{1, . . . , 16} and we define the atomic
propositions AP = {“blue”, “green”, “obs”, ∅} representing
goal (“blue” and “green”) and obstacle (“obs”) regions as
well as L(π5) = {“blue”}, L(π14) = {“green”}, L(π6) =
L(π10) = {“obs”} and L(πj) = ∅for the remaining regions.
Fig. 4(b) depicts the aforementioned workspace.
We consider the MITL formula φ = (□[0,∞)¬“obs”) ∧
♦[0,50](“green” ∧♦[0,20]“blue”), which represents the be-
havior of (i) always avoiding the obstacle regions and
(ii) eventually within 50s visiting the “green” region
and
after
20s
the
“blue”
region.
By
following
the
procedure
described
in
Section
IV-B,
we
obtain
the
accepting
timed
run
r
=
(πr1, t1)((πr2, t2)) · · ·
=
(π1, 0)(π2, 5)(π3, 10)(π4, 15)(π5, 20)(π12, 25)(π13, 30)
(π14, 35)(π11, 40)(π12, 45)(π5, 50).
Fig. 5.
The desired object trajectories (with green), the actual object
trajectories (with black), the domain specified by B(pd(t), l0) (with red)
and the domain specified by B(pO(t), ˆL), (with purple) for t ∈[0, 50]
sec. Since pO(t) ∈B(pd(t), l0), ∀t ∈[0, 50]s, the desired timed run is
successfully executed.
Regarding each transition πrj →πrj+1, j ∈{1, . . . , 10},
we chose ηd = [0, 0, 0]T , ρ0
sk = l0 = 0.5, ρ∞
sk = 0.01 and
lsk = 1 as well as ρ0
vk = 2|evk(tj)| + 0.1, ρ∞
vk = 0.01 and
lvk = 1, ∀k ∈{1, . . . , 6}. The control gains were chosen
as gsk = 0.1 and gv = 2.5, ∀k ∈{1, . . . , 6} to retain
the required input signals ui within feasible ranges that can
be implemented by real actuators. Finally, wO, wi and fi
were chosen as sinusoidal functions of time and the load
sharing coefficients were selected as c1 = 0.5, c2 = 0.35
and c3 = 0.15 to demonstrate a potential difference in the
power capabilities of the agents. Fig. 5 depicts the transitions
of the coupled system object-agents. It can be deduced from
the figure that pO ∈B(pd(t), l0), ∀t ∈[0, 50] and therefore
ps ∈πrj ∪πrj+1, ∀ps ∈Sq, j ∈{1, . . . , 10}, verifying thus
the theoretical results. Moreover, Fig. 6 shows the control
inputs of the three agents, demonstrating the effect of the
load sharing coefficients.
VI. CONCLUSION AND FUTURE WORK
In this work we proposed a hybrid control strategy for
the cooperative manipulation of an object by N agents
under MITL specifications. In particular, we developed a
robust decentralized control protocol that allowed us to
abstract the motion of the coupled system object-agents as a
finite transition system. Then, we employed standard formal-
verification tools for the derivation of a path that satisfied
the high level goal. Future efforts will be devoted towards
considering non-rigid grasps and compensating for uncertain
geometric characteristics of the objects.
REFERENCES
[1] Y.-H. Liu and S. Arimoto, “Decentralized adaptive and nonadaptive
position/force controllers for redundant manipulators in cooperations,”
International Journal of Robotics Research, 1998.
Fig. 6.
The resulting control inputs ui = [ui(1), . . . , ui(6)]T , i ∈
{1, 2, 3}. Top three plots: ui(1), ui(2), ui(3), for i = 1, 2, 3, respectively.
Bottom three plots: ui(4), ui(5), ui(6), for i = 1, 2, 3, respectively.
[2] F. Caccavale, P. Chiacchio, A. Marino, and L. Villani, “Six-dof
impedance control of dual-arm cooperative manipulators,” Transac-
tions on Mechatronics, 2008.
[3] D. Heck, D. Kostic, A. Denasi, and H. Nijmeijer, “Internal and
external force-based impedance control for cooperative manipulation,”
in European Control Conf., 2013.
[4] J. Szewczyk, F. Plumet, and P. Bidaud, “Planning and controlling
cooperating robots through distributed impedance,” JRS, 2002.
[5] A. Tsiamis, C. Verginis, C. Bechlioulis, and K. Kyriakopoulos, “Co-
operative manipulation exploiting only implicit communication,” in
Intern. Conf. on Intelligent Robots and Systems, 2015.
[6] A. Petitti, A. Franchi, D. D. Paola, and A. Rizzo, “Decentralized
motion control for cooperative manipulation with a team of networked
mobile manipulators,” ICRA, 2016.
[7] Z. Wang and M. Schwager, “Multi-robot manipulation with no com-
munication using only local measurements,” in CDC, 2015.
[8] T. G. Sugar and V. Kumar, “Control of cooperating mobile manipula-
tors,” Transactions on Robotics and Automation, 2002.
[9] H. G. Tanner, S. G. Loizou, and K. J. Kyriakopoulos, “Nonholonomic
navigation and control of cooperating mobile manipulators,” Transac-
tions on Robotics and Automation, 2003.
[10] S. Erhart and S. Hirche, “Adaptive force/velocity control for multi-
robot cooperative manipulation under uncertain kinematic parameters,”
in Intern. Conf. on Intelligent Robots and Systems, 2013.
[11] J. Markdahl, Y. Karayiannidis, and X. Hu, “Cooperative object path
following control by means of mobile manipulators: a switched
systems approach,” IFAC Proceedings Volumes, 2012.
[12] M. Guo, J. Tumova, and D. V. Dimarogonas, “Cooperative decen-
tralized multi-agent control under local ltl tasks and connectivity
constraints,” in Conf. on Decision and Control, 2014.
[13] Y. Chen, X. C. Ding, A. Stefanescu, and C. Belta, “Formal approach
to the deployment of distributed robotic teams,” TRO, 2012.
[14] Z. Zhang and R. V. Cowlagi, “Motion-planning with global temporal
logic specifications for multiple nonholonomic robotic vehicles,” in
Americal Control Conf., 2016.
[15] I. Filippidis and R. M. Murray, “Symbolic construction of gr(1)
contracts for systems with full information,” in ACC, 2016.
[16] Y. Diaz-Mercado, A. Jones, C. Belta, and M. Egerstedt, “Correct-by-
construction control synthesis for multi-robot mixing,” in CDC, 2015.
[17] R. Alur and D. L. Dill, “A theory of timed automata,” Theor. Comput.
Sci., 1994.
[18] R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing
punctuality,” Journal of the ACM, 1996.
[19] D. D’Souza and P. Prabhakar, “On the expressiveness of mtl in
the pointwise and continuous semantics,” International Journal on
Software Tools for Technology Transfer, 2007.
[20] A. Nikou, J. Tumova, and D. V. Dimarogonas, “Cooperative task
planning of multi-agent systems under timed temporal specifications,”
Americal Control Conf., 2016.
[21] S. Karaman and E. Frazzoli, “Linear temporal logic vehicle routing
with applications to multi-uav mission planning,” Intern. Journal of
Robust and Nonlinear Control, 2011.
[22] D. Aksaray, C.-I. Vasile, and C. Belta, “Dynamic routing of energy-
aware vehicles with temporal logic constraints,” ICRA, 2016.
[23] A. Yamashita, T. Arai, J. Ota, and H. Asama, “Motion planning of
multiple mobile robots for cooperative manipulation and transporta-
tion,” Trans. on Robotics and Automation, 2003.
[24] P. Cheng, J. Fink, and V. Kumar, “Abstractions and algorithms for
cooperative multiple robot planar manipulation,” Robotics: Science
and Systems IV, 2009.
[25] G. Lionis and K. J. Kyriakopoulos, “Centralized motion planning for
a group of micro agents manipulating a rigid object,” in MED, 2005.
[26] A. Tsiamis, J. Tumova, C. P. Bechlioulis, G. C. Karras, D. V.
Dimarogonas, and K. J. Kyriakopoulos, “Decentralized leader-follower
control under high level goals without explicit communication,” in
Intern. Conf. on Intelligent Robots and Systems, 2015.
[27] S. Chinchali, S. C. Livingston, U. Topcu, J. W. Burdick, and R. M.
Murray, “Towards formal synthesis of reactive controllers for dexter-
ous robotic manipulation,” in ICRA, 2012.
[28] K. He, M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “Towards
manipulation planning with temporal logic specifications,” in Intern.
Conf. on Robotics and Automation, 2015.
[29] L. Chaimowicz, M. Campos, and V. Kumar, “Hybrid systems modeling
of cooperative robots,” in ICRA, Sept 2003.
[30] B. Siciliano, L. Sciavicco, and L. Villani, Robotics : modelling,
planning and control.
Springer, 2009.
[31] E. D. Sontag, Mathematical control theory: deterministic finite dimen-
sional systems.
Springer Science & Business Media, 2013, vol. 6.
[32] C. P. Bechlioulis and G. A. Rovithakis, “A low-complexity global
approximation-free control scheme with prescribed performance for
unknown pure feedback systems,” Automatica, 2014.
[33] C. Baier, J.-P. Katoen et al., Principles of model checking. MIT press
Cambridge, 2008.