Model-Free Reinforcement Learning for Stochastic Games with Linear Temporal Logic Objectives

We study the problem of synthesizing control strategies for Linear Temporal (LTL) objectives in unknown environments. We model this problem as a-based zero-sum stochastic game between the controller and the environment, the transition probabilities and the model topology are fully unknown. winning condition for the controller in this game is the satisfaction of given LTL specification, which can be captured by the acceptance condition a deterministic Rabin automaton (DRA) directly derived from the LTL. We introduce a model-free reinforcement learning (RL) to find a strategy that maximizes the probability of satisfying a LTL specification when the Rabin condition of the derived DRA has a accepting pair. We then generalize this approach to LTL formulas for the Rabin condition has a larger number of accepting pairs, providing a bound on the satisfaction probability. Finally, we illustrate of our RL method on two motion planning case studies.