Logically-Constrained Neural Fitted Q-Iteration
This addresses the challenge of enforcing logical constraints in reinforcement learning for continuous domains, offering a novel integration of formal methods with neural networks, though it is incremental in combining existing techniques.
The paper tackles the problem of training Q-functions for continuous-state Markov Decision Processes to ensure policies satisfy Linear Temporal Logic properties, such as safety, and shows that the proposed method outperforms conventional approaches like MDP abstraction and approximate dynamic programming in a numerical study.
We propose a method for efficient training of Q-functions for continuous-state Markov Decision Processes (MDPs) such that the traces of the resulting policies satisfy a given Linear Temporal Logic (LTL) property. LTL, a modal logic, can express a wide range of time-dependent logical properties (including "safety") that are quite similar to patterns in natural language. We convert the LTL property into a limit deterministic Buchi automaton and construct an on-the-fly synchronised product MDP. The control policy is then synthesised by defining an adaptive reward function and by applying a modified neural fitted Q-iteration algorithm to the synchronised structure, assuming that no prior knowledge is available from the original MDP. The proposed method is evaluated in a numerical study to test the quality of the generated control policy and is compared with conventional methods for policy synthesis such as MDP abstraction (Voronoi quantizer) and approximate dynamic programming (fitted value iteration).