Reactive synthesis algorithms allow automatic construction of policies to
control an environment modeled as a Markov Decision Process (MDP) that are
optimal with respect to high-level temporal logic specifications. However, they
assume that the MDP model is known a priori. Reinforcement Learning (RL)
algorithms, in contrast, are designed to learn an optimal policy when the
transition probabilities of the MDP are unknown, but require the user to
associate local rewards with transitions. The appeal of high-level temporal
logic specifications has motivated research to develop RL algorithms for
synthesis of policies from specifications. To understand the techniques, and
nuanced variations in their theoretical guarantees, in the growing body of
resulting literature, we develop a formal framework for defining
transformations among RL tasks with different forms of objectives. We define
the notion of a sampling-based reduction to transform a given MDP into another
one which can be simulated even when the transition probabilities of the
original MDP are unknown. We formalize the notions of preservation of optimal
policies, convergence, and robustness of such reductions. We then use our
framework to restate known results, establish new results to fill in some gaps,
and identify open problems. In particular, we show that certain kinds of
reductions from LTL specifications to reward-based ones do not exist, and prove
the non-existence of RL algorithms with PAC-MDP guarantees for safety
specifications.

提出了一个形式框架，为定义不同形式目标的 RL 任务之间的转换提供了形式化定义，研究了这种转换的保持最优策略、收敛和稳健性的概念，证明了从 LTL 规范到基于奖励的规范的某些缩减不存在，证明了 RL 算法不存在 PAC-MDP 保证安全规范。