Abstract
We present a reinforcement learning (RL) framework to synthesize a controlpolicy from a given linear temporal logic (LTL) specification in an unknownstochastic environment that can be modeled as a Markov Decision Process (MDP).Specifically, we learn a policy that maximizes the probability of satisfyingthe LTL formula without learning the transition probabilities. We introduce anovel rewarding and path-dependent discounting mechanism based on the LTLformula such that (i) an optimal policy maximizing the total discounted rewardeffectively maximizes the probabilities of satisfying LTL objectives, and (ii)a model-free RL algorithm using these rewards and discount factors isguaranteed to converge to such policy. Finally, we illustrate the applicabilityof our RL-based synthesis approach on two motion planning case studies.