Linear temporal logic (LTL) is used to describe a complex control specification [1]}. In recent years, several automata-guided reinforcement learning (RL) have been investigated to synthesize an optimal controller for an unknown controlled stochastic system, e.g., Markov decision process (MDP), under an LTL specification [2]}, [3]}, [4]}, [5]}. They constructed the product MDP from the MDP and a Rabin or Büchi automaton converted from the LTL specification. An optimal controller was learned on the product MDP by maximizing the expected return with a reward assignments according to the acceptance condition. In [6]}, [7]}, truncated LTL specifications were used and rewards were assigned according to the converted automaton. Bounded synthesis is an alternative synthesis approach to avoid the state-complexity of Rabin automata [8]}. A bounded synthesis and reinforcement learning-based optimal controller synthesis for MDPs has been proposed [9]}.
