  The integration of reinforcement learning (RL) and formal methods has emerged
as a promising framework for solving long-horizon planning problems.
Conventional approaches typically involve abstraction of the state and action
spaces and manually created labeling functions or predicates. However, the
efficiency of these approaches deteriorates as the tasks become increasingly
complex, which results in exponential growth in the size of labeling functions
or predicates. To address these issues, we propose a scalable model-based RL
framework, called VFSTL, which schedules pre-trained skills to follow unseen
STL specifications without using hand-crafted predicates. Given a set of value
functions obtained by goal-conditioned RL, we formulate an optimization problem
to maximize the robustness value of Signal Temporal Logic (STL) defined
specifications, which is computed using value functions as predicates. To
further reduce the computation burden, we abstract the environment state space
into the value function space (VFS). Then the optimization problem is solved by
Model-Based Reinforcement Learning. Simulation results show that STL with value
functions as predicates approximates the ground truth robustness and the
planning in VFS directly achieves unseen specifications using data from
sensors.
