  This work investigates the formal policy synthesis of continuous-state
stochastic dynamic systems given high-level specifications in linear temporal
logic. To learn an optimal policy that maximizes the satisfaction probability,
we take a product between a dynamic system and the translated automaton to
construct a product system on which we solve an optimal planning problem. Since
this product system has a hybrid product state space that results in reward
sparsity, we introduce a generalized optimal backup order, in reverse to the
topological order, to guide the value backups and accelerate the learning
process. We provide the optimality proof for using the generalized optimal
backup order in this optimal planning problem. Further, this paper presents an
actor-critic reinforcement learning algorithm when topological order applies.
This algorithm leverages advanced mathematical techniques and enjoys the
property of hyperparameter self-tuning. We provide proof of the optimality and
convergence of our proposed reinforcement learning algorithm. We use neural
networks to approximate the value function and policy function for hybrid
product state space. Furthermore, we observe that assigning integer numbers to
automaton states can rank the value or policy function approximated by neural
networks. To break the ordinal relationship, we use an individual neural
network for each automaton state's value (policy) function, termed modular
learning. We conduct two experiments. First, to show the efficacy of our
reinforcement learning algorithm, we compare it with baselines on a classic
control task, CartPole. Second, we demonstrate the empirical performance of our
formal policy synthesis framework on motion planning of a Dubins car with a
temporal specification.
