Optimal Mission Planner with Timed Temporal Logic Constraints

arXiv:1510.01261v1 [cs.SY] 5 Oct 2015

Yuchen Zhou, Dipankar Maity and John S. Baras

Abstract— In this paper, we present an optimization based
method for path planning of a mobile robot subject to time
bounded temporal constraints, in a dynamic environment.
Temporal logic (TL) can address very complex task specification such as safety, coverage, motion sequencing etc. We use
metric temporal logic (MTL) to encode the task specifications
with timing constraints. We then translate the MTL formulae
into mixed integer linear constraints and solve the associated
optimization problem using a mixed integer linear program
solver. This approach is different from the automata based
methods which generate a finite abstraction of the environment
and dynamics, and use an automata theoretic approach to
formally generate a path that satisfies the TL. We have applied
our approach on several case studies in complex dynamical
environments subjected to timed temporal specifications.

I. I NTRODUCTION
Autonomous aircraft have been deployed for agriculture
research and management, surveillance and sensor coverage
for threat detection and disaster search and rescue operations.
All these applications require the tasks to be performed
in an optimal manner with specific timing constraints. The
high level task specifications for these applications generally
consist of temporal ordering of subtasks, motion sequencing
and synchronization etc. Given such specifications, it is
desirable to synthesize a reference trajectory that is both
optimal considering the dynamics of the vehicle and satisfies
the temporal constraints. Motion planning [1], [2], at its
early stage, considered optimal planning to reach a goal
from an initial position while avoiding obstacles [3]. New
techniques such as artificial potential functions [3], [4], cell
decomposition and probabilistic roadmaps [2] are introduced
for efficient planning in complex environment [5], [6] and
high dimensional state-space. However, these approaches
failed when task specifications have multiple goals or specific
ordering of goals, for example surveying some areas in
particular sequence.
Temporal logic [7]–[9] provides a compact mathematical
formulation for specifying such complex mission specifications. Previous approaches mainly focus on the usage of
linear temporal logic (LTL), which can specify tasks such
as visiting goals, periodically surveying areas, staying stable
and safe. The main drawback of the LTL formulation is that
it cannot specify time distance between tasks. In surveillance
examples, a simple task may be to individually monitor
*This work is supported by US AFOSR MURI grant FA9550-09-1-0538,
NSF grant CNS-1035655, NIST grant 70NANB11H148 and by DARPA
(through ARO) grant W911NF1410384.
The authors are with the Department of Electrical and Computer
Engineering, and the Institute for Systems Research, University of
Maryland, College Park, Maryland, USA. email: {yzh89, dmaity,

baras}@umd.edu

multiple areas for at least x amount of time. Additionally, the
LTL formulation commonly assumes the environment to be
static. Traditional approaches commonly start with creating a
finite abstraction of the environment including the dynamics,
then combine it with the automata that is generated from the
LTL specification [10]. The cell decomposition performed in
the abstraction process requires the environment to be static;
but in most situations this is not the case. For example, the
use of Unmanned Aerial Vehicles (UAVs) for surveillance in
the commercial airspace needs to consider motion of other
aircraft. The other weakness of the automata-based approach
is that it is computationally expensive. In this work, we are
interested in motion planning for surveillance in an airspace
with finite time task constraints and safety guarantees. For
this work, we only consider the other aircraft in the target
area as dynamic obstacles to the UAV. Further, we assume
that the motions of these dynamic obstacles can be either
predicted during the planning or are known a priori.
Due to the limitations of the previous approaches, we
instead present the method based on metric temporal logic
(MTL) [11], [12] and an optimization problem formulation
to solve the planning problem. MTL extends the LTL [7]
temporal operators so that it can express the requirements
on time distance between events and event durations. This
allows us to describe the dynamic obstacle and survey
durations in our case study.
An optimization based method for LTL was previously
proposed and extended by [13], [14]. In [13], the authors
propose to transform LTL specifications to mixed integer
constraints and solve the planning problem for finite horizon
using either a mixed integer linear program (MILP) or a
mixed integer quadratic program (MIQP) solver. In [14], the
algorithm is extended to infinite horizon so that trajectories
can contain loops. However, none of the methods consider
dynamic environment or moving obstacles, time varying
constraints, or duration of the tasks. MTL was used as a
temporal constraint to a routing planning problem in [15].
Their formulation unfortunately does not allow users to
incorporate dynamics of the vehicle.
In this paper, we consider a path planning problem for
surveillance under survey durations constraints for each
region and overall temporal constraint to visit each region
within given times. Our problem is considerably different
from the problems formulated in the existing literature in
the sense that we not only consider dynamic environment
but also associate each subtask with a duration constraint.
We generate a path that guarantee safety by avoiding static
and moving obstacles in the workspace and the path is
optimal in the sense that it minimizes a predefined cost

function. We do not adopt the linear encoding from [14],
since moving obstacles is not periodic in nature. Similar
to their approaches, we adopt the usage of mixed logic
dynamic (MLD) to model vehicle dynamics, so that the
overall problem is a MILP (considering linear cost function).
Our main contribution is usage of MTL to specify time
bounded tasks for the mission planner and reformulation of
the problem into a MILP. We also demonstrate the methods
on the case studies of using a quadrotor and ground vehicle
to survey multiple areas given the MTL specifications. The
rest of the paper is organized as follows. In section II we
present the fundamentals of MTL and define the overall
motion planning problem. We then formulate it into a mixed
integer linear optimization problem incorporating the temporal constraints in section III. Afterward, we demonstrate our
approach on motion planning for different simulation setups.
II. P RELIMINARIES
In this paper we consider a surveying task in an area by a
robot whose dynamics are given by the nonlinear model (1).
x(t + 1) = f (t, x(t), u(t))

(1)

where x(t) ∈ X , x(0) ∈ X0 ⊆ X , and u(t) ∈ U for all
t = 0, 1, 2, · · · . Let us denote the trajectory of the system
(1) starting at t0 with initial condition x0 and input u(t) as
xxt00 ,u = {x(s) |s ≥ t0 x(t + 1) = f (t, x(t), u(t)), x(t0 ) =
x0 }. For brevity, we will use xt0 instead of xxt00 ,u whenever
we do not need the explicit information about u(t) and x0 .
Definition 2.1: An atomic proposition is a statement
about the system variables (x) that is either True(>) or
False(⊥) for some given values of the state variables. [13]
Let Π = {π1 , π2 , · · · πn } be the set of atomic propositions
which labels X as a collection of survey areas, free space,
obstacles etc. The moving obstacles make the free space to
change from time to time, and hence labeling the environment is time dependent. We define a map that labels the time
varying environment as follows
L : X × I → 2Π

(2)

where I = {[a, b]| b > a ≥ 0} and 2Π is denoted as the
power set of Π. In general, I is used to denote a time interval
but it can be used to denote a time instance as well.
The trajectory of the system is a sequence of states such
that each state x(t) stays in X for all t and there exists u(t) ∈
U for all t such that x(t + 1) = f (t, x(t), u(t)). Corresponding to each trajectory x0 , the sequence of atomic proposition
satisfied is given by L(x0 ) = L(x(0), 0)L(x(1), 1)...
The high level specification of the surveying task will be
expressed formally using MTL which can incorporate timing
specifications.
A. Metric Temporal Logic (MTL)
Metric temporal logic, a member of temporal logic family,
deals with model checking under timing constraints. The
formulas for MTL are build on atomic propositions by
obeying some grammar.

Definition 2.2: The syntax of MTL formulas are defined
according to the following grammar rules:
φ ::= > | π | ¬φ | φ ∨ φ | φUI φ
where I ⊆ [0, ∞] is an interval with end points in N ∪ {∞}.
π ∈ Π, > and ⊥(= ¬>) are the Boolean constants true and
f alse respectively. ∨ denotes the disjunction operator and
¬ denotes the negation operator. UI symbolizes the timed
Until operator. Sometimes we will represent U[0,∞] by U.
Other Boolean and temporal operators such as conjunction
(∧), eventually within I (♦I ), always on I (I ) etc. can
be represented using the grammar desired in definition 2.2.
For example, we can express time constrained eventually
operator ♦I φ ≡ >UI φ and so on.
Definition 2.3: The semantics of any MTL formula φ is
recursively defined over a trajectory xt as:
xt |= π iff π ∈ L(x(t), t)
xt |= ¬π iff π ∈
/ L(x(t), t)
xt |= φ1 ∨ φ2 iff xt |= φ1 or xt |= φ2
xt |= φ1 ∧ φ2 iff xt |= φ1 and xt |= φ2
xt |= φ iff xt+1 |= φ
xt |= φ1 UI φ2 iff ∃s ∈ I s.t. xt+s |= φ2 and ∀ s0 ≤
s, xt+s0 |= φ1 .
Thus, the expression φ1 UI φ2 means that φ2 will be true
within time interval I and until φ2 becomes true φ1 must
be true. Similarly, the release operator φ1 Rφ2 denotes the
specification that φ2 should always hold and it can be
released only when φ1 is true. The MTL operator φ means
that the specification φ is true at next time instance, I φ
means that φ is always true for the time duration I, ♦I φ
means that φ will eventually become true within the time
interval I. Composition of two or more MTL operators
can express very sophisticated specifications; for example
♦I1 I2 φ means that within time interval I1 , φ will be true
and from that instance it will hold true always for a duration
of I2 . Other Boolean operators such as implication (⇒)
and equivalence (⇔) can be expressed using the grammar
rules and semantics given in definitions 2.2 and 2.3. More
details on MTL grammar and semantics can be found in [11].
Satisfaction of a temporal specification φ by a trajectory xt0
will be denoted as xt0 |= φ.
III. P ROBLEM F ORMULATION AND S OLUTION
We consider a planning problem to periodically survey
some selected areas in a given workspace. There are specific
time bounds, associated with the regions, by which the
surveillance has to be finished. Given the system dynamics
(1), the objective is to find a suitable control law that
will steer the robot in the survey area so that all regions
are surveyed within the time bound and that control will
optimize some cost function as well. The surveying task and
its associated timing constraints and safety constraints can
be expressed formally by Metric Temporal Logic (MTL).
Let φ denote the MTL formula for the surveying task, and
J(x(t, u), u) be a cost function to make the path optimal in
some sense. We formally present our planning objective as
an optimization problem given in Problem (3.1)

Problem 3.1:
min

J(x(t, u), u(t))

u

x(t + 1) = f (t, x(t), u(t))
xt0 |= φ
In the following section we are going to discuss the linearization techniques for the dynamics of the robot, and our
approach to translate an MTL constraint as linear constraints.
subject to

A. Linearized Dynamics of the Robot
Since we are interested in solving the planning problem
as an optimization problem with mixed integer and linear
constraints, we need to represent the dynamics of the robot
as a linear constraint to the optimization problem (3.1). We
will consider surveying some given areas by ground robots as
well as aerial robots. The dynamics of the autonomous aerial
robot and ground robot are given in (3) and (4) respectively.
1) Quadrotor Model: To capture the dynamics of the
quadrotor properly, we need two coordinate frames. One of
them is a fixed frame and will be named as earth frame,
and the second one is body frame which moves with the
quadrotor. The transformation matrix from body frame to
earth frame is R(t). The quadrotor dynamics has twelve
state variables (x, y, z, vx , vy , vz , φ, θ, ψ, p, q, r), where ξ =
[x, y, z]T and v = [vx , vy , vz ]T represent the position and
velocity of the quadrotor w.r.t the body frame. (φ, θ, ψ) are
the roll, pitch and yaw angle, and Ω = [p, q, r]T are the rates
of change of roll, pitch and yaw respectively.
The Newton-Euler formalism for the quadrotor rigid body
dynamics in earth fixed frame is given by:
ξ˙ = v
v̇ = −ge3 +

F
Re3
m

(3)

Ṙ = RΩ̂
Ω̇ = J −1 (−Ω × JΩ + u)
where g is the acceleration due to gravity, e3 = [0, 0, 1]T , F
is the total lift force and u = [u1 , u2 , u3 ]T are the torques
applied. F and u are the control inputs. More details on
the quadrotor dynamics can be found in [16], [17]. For this
work, we linearize the dynamics (3) about the hover with
yaw constraint to be zero, as it has been done in [14]. Since
ψ is constrained to be zero, we remove ψ and r from our
system and make the system ten dimensional. Consequently,
we only need three control inputs, F, u1 , and u2 for the
system. The linearized model is the same as what is done in
[14], 
[18]. The system matrices
 for thelinearized model are:

0 I  0  0
0
 0 

 0


0 g




0 0 −g 0 0
 0 

0
; B = 

A=




0 0


 1/m

0 0



0
I
0
0
−1
0
I2×3 J
0 0
0
0
1 0 0
I2,3 =
0 1 0
All zero and identity matrices in A and B are of proper
dimensions.

2) Car-Like Model: We also investigate our approach on
a car-like dynamical system (4). The system has three state
variables: positions (x, y), heading angle θ.

 


ẋ
cos(θ) 0 
 ẏ  =  sin(θ) 0  u1
(4)
u2
0
1
θ̇
where u1 and u2 are the control inputs. We linearize this
nonlinear model about several values for θ and depending
on the value of θ, the closest linearization was used to drive
the linearized system. The linearization is similar to what is
suggested in [14]. The linearized system matrices at θ̂ are
given by:




0 0 −û1 sin(θ̂)
cos(θ̂) 0
A = 0 0 û1 cos(θ̂)  ; B =  sin(θ̂) 0
0 0
0
0
1
B. Mixed Integer Linear Constraints
In this section, we demonstrate our approach to translate a
time-bounded temporal logic formula to linear constraints on
state variables and inputs. The easiest example of it would be
how to express the temporal constraint that x(t) lies within
a convex polygon P at time t. This simple example will
serve as a building block for other complicated temporal
operators. Any convex polygon P can be represented as an
intersection of several halfspaces. A halfspace is expressed
by a set of points, Hi = {x : hTi x ≤ ki }. Thus, x(t) ∈ P
is equivalent to x(t) ∈ ∩ni=1 Hi = ∩ni=1 {x : hTi x ≤ ki }.
The temporal constraint that x(t) will be inside P for all
t ∈ {t1 , t1 + 1, · · · t1 + n} can be represented by the set of
linear constraints {hTi x(t) ≤ ki } for all i = {1, 2, · · · , n}
and ∀t ∈ {t1 , t1 + 1, · · · t1 + n}.
We adopted a method similar to the method used in [13]
to translate temporal constraint φ into mixed integer linear
constraints. We extend it to incorporate duration for task
completion and loop constraints of the trajectory. Comparing
to [14], we only enforce the loop constraints at the trajectory
level instead of the temporal logic level, since the moving
obstacles is not periodic in nature. The planning process will
be repeated when the vehicle returns to the initial point.
In a polygonal environment, atomic propositions (AP), p ∈
Π, can be related to states of the system using disjunction and
conjunction of halfspaces. In other words, the relationship
between measured outputs such as location of the vehicle and
the halfspaces defines the proposition used in the temporal
logics. Consider the convex polygon case and let zit ∈ {0, 1}
be the binary variables associated with halfspaces {x(t) :
hTi x(t) ≤ ki } at time t = 0, ..., N . We enforce the following
constraint zit = 1 if and only if hTi x(t) ≤ ki by adding the
linear constraints,
hTi x(t) ≤ ki + M (1 − zit )

(5)

hTi x(t) ≥ ki − M zit + 
where M is a large positive number and  is a small positive
number. If we denote PtP = ∧ni=1 zit , then PtP = 1 if and
only if x(t) ∈ P. This can be extended to the nonconvex

case by decomposing the polygon to convex ones and linking
them using disjunction operators. As discussed later in this
section, the disjunction operator can also be translated to
mixed integer linear constraints.
We will use Fφ (x, z, u, t) to denote the set of all mixed
integer linear constraints corresponding to the temporal logic
formula φ. Once we have formulated Fp (x, z, u, t) for atomic
propositions p, we can find Fφ (x, z, u, t) for any MTL
formula φ. The next essential part of the semantics of MTL
is the Boolean operations, such as ¬, ∧, ∨. Similarly these
operators can be translated into linear constraints. Let t ∈
{0, 1, ..., N }, Ptφ be the continuous variables within [0,1]
associated with formula φ made up with propositions p ∈ Π
at time t.
• φ = ¬p is the negation of an atomic proposition, and it
can be modeled as
Ptφ = 1 − Ptp .
•

(6)

The conjunction operation, φ = ∧m
i=1 pi , is modeled as
Ptφ ≤ Ptpi ,

i = 1, ..., m,
m
X
Ptpi ,
Ptφ ≥ 1 − m +

(7)

(8)

i=1

Similarly, the temporal operators can be modeled using
linear constraints as well. Let t ∈ {0, 1, ..., N − t2 }, where
[t1 , t2 ] is the time interval used in the MTL.
• Eventually: φ = ♦[t1 ,t2 ] p is equivalent to
Ptφ ≥ Pτp ,
Ptφ ≤

t+t
X2

τ ∈ {t + t1 , ..., t + t2 }

(9)

Always: φ = [t1 ,t2 ] p is equivalent to
Ptφ ≤ Pτp ,
Ptφ ≥

t+t
X2

τ ∈ {t + t1 , ..., t + t2 }

(10)

Pτp − (t2 − t1 ),

τ =t+t1
•

Until: φ = pU[t1 ,t2 ] q is equivalent to
atj ≤ Pqj
atj ≤

Ppk




(∧k=j−1
Ppk ) ∧ Pqj .
k=t

Other combinations for different temporal operators are also
straight forward and we are not enumerating them for the
sake of space, but one can easily derive them by using (6)
through (11).
Using this approach, we translate the given high level specification in MTL (xt0 |= φ) to a set of mixed integer linear
constraints Fφ (x, z, u, t). At the end, we add the constraint
P0φ = 1, i.e. the overall specification φ is satisfied. Since
Boolean variables are only introduced when halfspaces are
defined, the computation cost of MILP is at most exponential
to the number of halfspaces times the discrete steps N .
IV. C ASE S TUDY AND D ISCUSSION

Pτp

τ =t+t1
•

=

t+t
_2
j=t+t1

The disjunction operator, φ = ∨m
i=1 pi , is modeled as
Ptφ ≥ Ptpi , i = 1, ..., m,
m
X
Ptφ ≤
Ptpi ,

The until formulation (11) is obtained similarly to [13]. For
MTL, it is modified by noticing the following equality,
Ptφ

i=1
•

Fig. 1. Workspace setup of the first test case. Blue area represents an
obstacle moving from right to left. Grey areas represent static obstacles.
Green areas represent survey areas used in the temporal logic. The shaded
areas around obstacles represent boundary of the obstacles for discrete
planning, so that the obstacles can be avoided even for continuous dynamics.
The resulting 2D trajectory of the quadrotor for φ1 is shown as blue dots.
The resulting motion is counter clockwise.

j ∈ {t + t1 , · · · , t + t2 },
k ∈ {t, · · · , j − 1}, j ∈ {t + t1 , · · · , t + t2 },

We apply our method for solving mission planning with
finite time constraints on two different workspaces. Both
workspaces contain static and moving obstacles.The experiments are run through YALMIP-CPLEX on a computer
with 3.4GHz processor and 8GB memory. We performed the
simulation for both a quadrotor model and a car model.
The first environment is the one shown in Fig. 1, where
blue and gray areas represent moving and static obstacles
respectively, and green areas represent survey targets.
Let the temporal specification be the following
φ1 = ♦[0,2] A ∧ ♦[0,2] B ∧ ♦[0,2] C ∧ ¬O

φ2 = ♦[0,2] A ∧ ♦[0,2] B ∧ ♦[0,2] C ∧ ¬O ∧ ¬B U[0,N ] A
Ppk − (j − t) j ∈ {t + t1 , · · · , t + t2 }, where O represents the static and moving obstacles, N is the
k=t
horizon of the planning trajectory. Such N can be generally
t+t
2
X
obtained by performing a feasibility test using MILP solver
Ptφ ≤
atj ,
(11)
starting from N = 2, and increasing N until finding a
j=t+t1
feasible one. For the purpose of comparing different temporal
Ptφ ≥ atj j ∈ {t + t1 , · · · , t + t2 }.
constraints, we choose a feasible horizon N = 50 for both
atj ≥ Pqj +

j−1
X

Fig. 2. Time-state-space representation of the environment and resulting
trajectory for the quadrotor with temporal constraints φ1 . The vehicle starts
from (0.5,0.5) and surveys area b, c and a sequentially.

Fig. 3. Time-state-space representation of the environment and resulting
trajectory for the quadrotor with temporal constraints φ2 . Because of the
additional ordering requirement, the vehicle covers area a first before visiting
area b.

MTL specifications φ1 and φ2 . The specification φ1 requires
the vehicle to visit areas A, B and C eventually and stay
there for at least 2 time units, while avoiding obstacles O.
φ2 adds an additional requirement on the ordering between A
and B, so that region A has to be visited first.
PN We consider
the cost function, J, to be minimized is t=0 |u(t)|. The
dynamics of the vehicles are discretized at a rate of 2Hz.
The resulting trajectory for the quadrotor with temporal
specification φ1 is plotted in time-state-space in Fig. 2. The
projection of the trajectory on the workspace is shown in
Fig. 1. The motion of the quadrotor in Fig. 1 is counter
clockwise. The quadrotor safely avoids the moving obstacle
by navigating through the area after the obstacle passes.
The survey duration in individual area also satisfies the
requirements as shown in Fig. 1. The quadrotor stays within
each survey area for 5 discrete time units which is equivalent
to 2s duration. These plots show a better realization of
visiting individual areas comparing to [13] and [14]. In their
results, trajectory visits targeted areas for only 1 discrete
time unit which is not desired for most surveillance tasks.
Additional local planning is possible to generate a sweeping
pattern so that the target areas can be covered by onboard
sensors in designed durations.
The resulting trajectory for the vehicle with specification
φ2 is shown in time-state-space in Fig. 3. As can be verified
from the trajectory, the vehicle travels first to area A before

Fig. 4. Time-state-space representation of the environment and resulting
trajectory for the car model with temporal constraints φ1 . The result for φ2
is similar since the optimal solution for φ1 already goes through area A
first.

Fig. 5. Workspace setup of the second test case. The moving obstacle
moves from the the bottom left corner to upper right corner. 2D trajectory
of the vehicle is shown as blue dots. The resulting motion is clockwise.

visiting B as specified. The CPLEX solver returns the
solution for the first trajectory in 20.8 sec while the second
one takes 34.7 sec. The additional continuous variables used
in the until encoding have large influence in the performance.
One of the possible future research directions would be
finding different encoding of the until operator to improve
the speed of the algorithm.
The result of specification φ1 for the car model is shown
in Fig. 4, where the small blue arrow associated with each
blue dot indicates the instantaneous heading of the vehicle.
The computation time is 150s. The longer computation time
is caused by the additional binary variables introduced by
the linearization of the dynamics at various heading angles.
The second environment considers a fast moving obstacle
that moves across the workspace diagonally, and hence the
vehicle has to adjust its motion accordingly. The environment
is shown in Fig 5. Similar to the previous example, it shows
the motion of the moving obstacle, static obstacles and
survey areas.
The temporal logic specifications are similar to the previous one but have an additional area to be visited. We also
tested the case when certain area has to be visited first. The
result is similar to previous cases, so we only show the plots

Fig. 6. Time-state-space representation of the environment and resulting
trajectory for the quadrotor with temporal constraints φ3 . The planned
trajectory is very close to the dynamic obstacles.

problem as a Linear Programming problem. We have considered polygonal environments for our case studies, but if the
environment is not polygonal, one can approximate it with a
polygonal environment. We have used a binary variable (z)
with each halfspace, so if the polygonal approximation of
the environment contains too many halfspaces, the problem
would be complex.
Due to space constraints, we have reported the case studies
only for quadrotor and car dynamics. The simulation results
show promising performance of our approach to find an
optimal solution. We consider dynamic but deterministic environments and uncertainties in the dynamics of the robot are
also not considered. There are many possible directions such
as planning in uncertain environment, stochastic dynamics of
the robots or multi-robot cooperative planning that one might
consider as an extension of this framework.
R EFERENCES

Fig. 7. Time-state-space representation of the environment and resulting
trajectory for the car model with temporal constraints φ3 . The result for φ4
is the same since the optimal solution already goes through A first.

for φ3 .
φ3 = ♦[0,2] A ∧ ♦[0,2] B ∧ ♦[0,2] C ∧ ♦[0,2] D ∧ ¬O
The resulting trajectory in time-state-space for the quadrotor with temporal specification φ3 is plotted in Fig. 6. The
projected trajectory on the workspace of the robot is shown
in Fig. 5. The motion of the vehicle is clockwise in Fig.
5. As can be seen from Fig. 6, the quadrotor safely avoids
the moving obstacle and the static ones nearby. The survey
duration in individual area also satisfies the requirements
as shown in Fig. 5. The computation time is 138.8s. The
increase in computation time is because the complex environment introduces more binary variables.
The result of specification φ3 for the car model is shown
in Fig. 7, where the blue arrows indicate the heading of the
vehicle. The computation time is 500s.
V. C ONCLUSION
In this paper, we have presented an optimization based
approach to plan the trajectory of a robot in a dynamic
environment to perform some temporal task with finite time
constraints. Our approach is simple in the sense that it
translates the time constraints and the temporal specifications
as linear constraints on the state and input variables. We have
linearized the dynamics of the robot in order to formulate the

[1] J. Latombe, Robot motion planning, ser. Kluwer international series
in engineering and computer science. Boston: Kluwer Academic
Publishers, 1991.
[2] S. M. LaValle, Planning algorithms. Cambridge university press,
2006.
[3] H. M. Choset, Principles of robot motion: theory, algorithms, and
implementation. MIT press, 2005.
[4] W. Xi, X. Tan, and J. S. Baras, “A hybrid scheme for distributed control
of autonomous swarms,” in Proceedings of the 2005 American Control
Conference. IEEE, 2005, pp. 3486–3491.
[5] R. Sharma, “Locally efficient path planning in an uncertain, dynamic
environment using a probabilistic model,” Robotics and Automation,
IEEE Transactions on, vol. 8, no. 1, pp. 105–110, 1992.
[6] S. M. LaValle and R. Sharma, “On motion planning in changing, partially predictable environments,” The International Journal of Robotics
Research, vol. 16, no. 6, pp. 775–805, 1997.
[7] C. Baier, J.-P. Katoen et al., Principles of model checking. MIT press
Cambridge, 2008, vol. 26202649.
[8] E. M. Clarke, O. Grumberg, and D. Peled, Model checking. MIT
press, 1999.
[9] M. M. Quottrup, T. Bak, and R. Zamanabadi, “Multi-robot planning:
A timed automata approach,” in Robotics and Automation, 2004.
Proceedings. ICRA’04. 2004 IEEE International Conference on, vol. 5.
IEEE, 2004, pp. 4417–4422.
[10] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logicbased reactive mission and motion planning,” IEEE Transactions on
Robotics, vol. 25, no. 6, pp. 1370–1381, 2009.
[11] R. Koymans, “Specifying real-time properties with metric temporal
logic,” Real-time systems, vol. 2, no. 4, pp. 255–299, 1990.
[12] J. Ouaknine and J. Worrell, “Some recent results in metric temporal
logic,” in Formal Modeling and Analysis of Timed Systems. Springer,
2008, pp. 1–13.
[13] S. Karaman, R. G. Sanfelice, and E. Frazzoli, “Optimal control of
mixed logical dynamical systems with linear temporal logic specifications,” in 47th IEEE Conference on Decision and Control. IEEE,
2008, pp. 2117–2122.
[14] E. M. Wolff, U. Topcu, and R. M. Murray, “Optimization-based
trajectory generation with linear temporal logic specifications,” in Int.
Conf. on Robotics and Automation, 2014.
[15] S. Karaman and E. Frazzoli, “Vehicle routing problem with metric
temporal logic specifications,” in Decision and Control, 2008. CDC
2008. 47th IEEE Conference on. IEEE, 2008, pp. 3953–3958.
[16] N. Michael, D. Mellinger, Q. Lindsey, and V. Kumar, “The grasp
multiple micro-uav testbed,” IEEE Robotics & Automation Magazine,
vol. 17, no. 3, pp. 56–65, 2010.
[17] L. R. Garcı́a Carrillo, A. E. Dzul López, R. Lozano, and C. Pégard,
“Modeling the quad-rotor mini-rotorcraft,” Quad Rotorcraft Control,
pp. 23–34, 2013.
[18] D. J. Webb and J. van den Berg, “Kinodynamic rrt*: Asymptotically
optimal motion planning for robots with linear dynamics,” in 2013
IEEE International Conference on Robotics and Automation (ICRA).
IEEE, 2013, pp. 5054–5061.

