Linear Temporal Logic (LTL) is widely used to specify high-level objectives for system policies, and it is highly desirable for autonomous systems to learn the optimal policy with respect to such specifications. However, learning the optimal policy from LTL specifications is not trivial. We present a model-free Reinforcement Learning (RL) approach that efficiently learns an optimal policy for an unknown stochastic system, modelled using Markov Decision Processes (MDPs). We propose a novel and more general product MDP, reward structure and discounting mechanism that, when applied in conjunction with off-the-shelf model-free RL algorithms, efficiently learn the optimal policy that maximizes the probability of satisfying a given LTL specification with optimality guarantees. We also provide improved theoretical results on choosing the key parameters in RL to ensure optimality. To directly evaluate the learned policy, we adopt probabilistic model checker PRISM to compute the probability of the policy satisfying such specifications. Several experiments on various tabular MDP environments across different LTL tasks demonstrate the improved sample efficiency and optimal policy convergence.

翻译：线性时序逻辑（LTL）被广泛用于系统策略的高层级目标规范，而自主系统迫切需要学习满足此类规范的最优策略。然而，从LTL规范中学习最优策略并非易事。我们提出了一种无模型强化学习方法，能够针对以马尔可夫决策过程（MDP）建模的未知随机系统高效学习最优策略。通过设计新颖且更具一般性的乘积MDP、奖励结构及折扣机制，结合现成的无模型强化学习算法，我们可高效学习能最大化满足给定LTL规范概率的最优策略，并附带最优性保证。此外，我们改进了强化学习中关键参数选取的理论依据，确保策略的最优性。为直接评估所学策略，我们采用概率模型检验工具PRISM计算策略满足规范的概率。在多种表格型MDP环境及不同LTL任务上的实验表明，该方法在样本效率与最优策略收敛性方面均实现了显著提升。