Logically-Constrained Neural Fitted Q-Iteration

TL;DR

This paper introduces a neural fitted Q-iteration method constrained by linear temporal logic to synthesize policies in continuous-state MDPs, ensuring time-dependent properties are satisfied, with evaluations showing its effectiveness.

Contribution

It presents a novel approach combining LTL constraints with neural fitted Q-iteration for policy synthesis in continuous MDPs, without prior knowledge of the environment.

Findings

Effective policy synthesis satisfying LTL properties

Comparison shows advantages over traditional methods

Numerical results validate the approach

Abstract

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).