LTL-Constrained Policy Optimization with Cycle Experience Replay

TL;DR

This work introduces Cycle Experience Replay (CyclER), a novel reward shaping technique that exploits the underlying structure of the LTL constraint to guide a policy towards satisfaction by encouraging partial behaviors compliant with the constraint.

Abstract

Linear Temporal Logic (LTL) offers a precise means for constraining the behavior of reinforcement learning agents. However, in many settings where both satisfaction and optimality conditions are present, LTL is insufficient to capture both. Instead, LTL-constrained policy optimization, where the goal is to optimize a scalar reward under LTL constraints, is needed. This constrained optimization problem proves difficult in deep Reinforcement Learning (DRL) settings, where learned policies often ignore the LTL constraint due to the sparse nature of LTL satisfaction. To alleviate the sparsity issue, we introduce Cycle Experience Replay (CyclER), a novel reward shaping technique that exploits the underlying structure of the LTL constraint to guide a policy towards satisfaction by encouraging partial behaviors compliant with the constraint. We provide a theoretical guarantee that optimizing CyclER will achieve policies that satisfy the LTL constraint with near-optimal probability. We evaluate CyclER in three continuous control domains. Our experimental results show that optimizing CyclER in tandem with the existing scalar reward outperforms existing reward-shaping methods at finding performant LTL-satisfying policies.

Figures (14)

• Figure 1: Left: The FlatWorld MDP and an example trajectory. Right: An LDBA for the LTL formula $\varphi = G (F(r) \& F(g) \& F(y)) \& G( \neg b)$ (some edges omitted for readability); the accepting state 0 is coded in green. The CyclER method considers all accepting paths within an LDBA and selects the most reward-ful path for the trajectory to shape LTL reward. Unlike previous approaches Camacho2019LTLAndBeyondvoloshin2023eventual, CyclER offers dense reward, even without visiting the accepting state.
• Figure 2: Trajectories from unshaped $r_{\text{DUAL}}$ (left) and CyclER $r_{\text{DUAL}}$ (right) for the formula $G (F(r) \& F(g) \& F(y))$$\&$$G( \neg b)$.
• Figure 3: Training curves showing unshaped $r_{\text{LTL}}$ (top) and $r_{\text{MDP}}$ (bottom) performance averaged over 5 random seeds. Each point is the mean of 10 stochastic policy rollouts.
• Figure 4: Training curves showing the shaped$r_{\text{LTL}}$ achieved by CyclER-learned policies, averaged over 5 random seeds. Each point is the mean of 10 stochastic policy rollouts.
• Figure 5: Sample trajectories from each baseline method in the FlatWorld domain (each row is a different seed). CyclER is able to consistently learn behavior that repeatedly visits and accepting state. The LCER baseline cannot achieve this long horizon task and instead optimizes for $r_{\text{MDP}}$. The LCER (no $r_{\text{MDP}})$ baseline, even when successful in visiting the accepting state (bottom right), does qualitatively learn satisfying behavior despite visiting the accepting state.

Theorems & Definitions (16)

• Definition 2.1: Acceptance of $\xi$
• Definition 2.2: Product MDP
• Definition 2.3: Trajectory acceptance
• Definition 2.4: Policy satisfaction
• Definition 2.5: Probability-optimal policies
• Theorem 3.2
• Definition 4.1: Accepting Initial Path (AIP)
• Definition 4.2: Accepting Cycle (AC)
• Definition 4.3: Minimal AIP (MAIP)
• Definition 4.4: Minimal AC (MAC)