HypRL: Reinforcement Learning of Control Policies for Hyperproperties
This addresses the problem of specifying and optimizing multi-agent objectives for researchers in formal methods and reinforcement learning, representing a novel method for a known bottleneck.
The paper tackles the challenge of reward shaping in multi-agent reinforcement learning for complex tasks by proposing HYPRL, a framework that learns control policies for hyperproperties expressed in HyperLTL, achieving improved efficiency and effectiveness in benchmarks like safety-aware planning and Deep Sea Treasure.
Reward shaping in multi-agent reinforcement learning (MARL) for complex tasks remains a significant challenge. Existing approaches often fail to find optimal solutions or cannot efficiently handle such tasks. We propose HYPRL, a specification-guided reinforcement learning framework that learns control policies w.r.t. hyperproperties expressed in HyperLTL. Hyperproperties constitute a powerful formalism for specifying objectives and constraints over sets of execution traces across agents. To learn policies that maximize the satisfaction of a HyperLTL formula $φ$, we apply Skolemization to manage quantifier alternations and define quantitative robustness functions to shape rewards over execution traces of a Markov decision process with unknown transitions. A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward and, consequently, increase the probability of satisfying $φ$. We evaluate HYPRL on a diverse set of benchmarks, including safety-aware planning, Deep Sea Treasure, and the Post Correspondence Problem. We also compare with specification-driven baselines to demonstrate the effectiveness and efficiency of HYPRL.