This paper addresses the problem of designing optimal control policies for
mobile robots with mission and safety requirements specified using Linear
Temporal Logic (LTL). We consider robots with unknown stochastic dynamics
operating in environments with unknown geometric structure. The robots are
equipped with sensors allowing them to detect obstacles. Our goal is to
synthesize a control policy that maximizes the probability of satisfying an
LTL-encoded task in the presence of motion and environmental uncertainty.
Several deep reinforcement learning (DRL) algorithms have been proposed
recently to address similar problems. A common limitation in related works is
that of slow learning performance. In order to address this issue, we propose a
novel DRL algorithm, which has the capability to learn control policies at a
notably faster rate compared to similar methods. Its sample efficiency is due
to a mission-driven exploration strategy that prioritizes exploration towards
directions that may contribute to mission accomplishment. Identifying these
directions relies on an automaton representation of the LTL task as well as a
learned neural network that (partially) models the unknown system dynamics. We
provide comparative experiments demonstrating the efficiency of our algorithm
on robot navigation tasks in unknown environments.

通过自动机表示 LTL 任务以及部分模拟未知系统动力学的神经网络，我们提出了一种新颖的深度强化学习（DRL）算法，其样本效率得以提高，能够更快速地学习控制策略，以在未知环境中的机器人导航任务中提高效率。

面向任务驱动的探索，加速具有时态逻辑任务规范的深度强化学习

Mission-driven Exploration for Accelerated Deep Reinforcement Learning  with Temporal Logic Task Specifications

Several methods have been proposed recently to learn neural network (NN)
controllers for autonomous agents, with unknown and stochastic dynamics, tasked
with complex missions captured by Linear Temporal Logic (LTL). Due to the
sample-inefficiency of the majority of these works, compositional learning
methods have been proposed decomposing the LTL specification into smaller
sub-tasks. Then, separate controllers are learned and composed to satisfy the
original task. A key challenge within these approaches is that they often lack
safety guarantees or the provided guarantees are impractical. This paper aims
to address this challenge. Particularly, we consider autonomous systems with
unknown and stochastic dynamics and LTL-encoded tasks. We assume that the
system is equipped with a finite set of base skills modeled by trained NN
feedback controllers. Our goal is to check if there exists a temporal
composition of the trained NN controllers - and if so, to compute it - that
will yield a composite system behavior that satisfies the assigned LTL task
with probability one. We propose a new approach that relies on a novel
integration of automata theory and data-driven reachability analysis tools for
NN-controlled stochastic systems. The resulting neuro-symbolic controller
allows the agent to generate safe behaviors for unseen complex temporal logic
tasks in a zero-shot fashion by leveraging its base skills. We show correctness
of the proposed method and we provide conditions under which it is complete. To
the best of our knowledge, this is the first work that designs verified
temporal compositions of NN controllers for unknown and stochastic systems.
Finally, we provide extensive numerical simulations and hardware experiments on
robot navigation tasks to demonstrate the proposed method.

该论文介绍了一种解决具有未知和随机系统动力学以及 LTL 编码任务的神经网络控制器的时间组合问题的新方法，该方法整合了自动机理论和数据驱动的可达性分析工具，通过基本技能的复合生成安全行为，通过数值模拟和实验验证了该方法。