  Path planning for a robot is one of the major problems in the area of
robotics. When a robot is given a task in the form of a Linear Temporal Logic
(LTL) specification such that the task needs to be carried out repetitively, we
want the robot to follow the shortest cyclic path so that the number of times
the robot completes the mission within a given duration gets maximized. In this
paper, we address the LTL path planning problem in a dynamic environment where
the newly arrived dynamic obstacles may invalidate some of the available paths
at any arbitrary point in time. We present DT*, an SMT-based receding horizon
planning strategy that solves an optimization problem repetitively based on the
current status of the workspace to lead the robot to follow the best available
path in the current situation. We implement our algorithm using the Z3 SMT
solver and evaluate it extensively on an LTL specification capturing a
pick-and-drop application in a warehouse environment. We compare our SMT-based
algorithm with two carefully crafted greedy algorithms. Our experimental
results show that the proposed algorithm can deal with the dynamism in the
workspace in LTL path planning effectively.
