Graph Contextual Reinforcement Learning for Efficient Directed Controller Synthesis

TL;DR

This paper introduces GCRL, a novel method combining graph neural networks with reinforcement learning to improve the efficiency and generalization of controller synthesis for labeled transition systems.

Contribution

GCRL integrates graph neural networks into RL-based exploration policies, capturing broader context for more efficient controller synthesis.

Findings

GCRL outperforms state-of-the-art methods in four of five benchmarks.

GCRL demonstrates improved learning efficiency and generalization.

Performance drops in highly symmetric, locally-interacting domains.

Abstract

Controller synthesis is a formal method approach for automatically generating Labeled Transition System (LTS) controllers that satisfy specified properties. The efficiency of the synthesis process, however, is critically dependent on exploration policies. These policies often rely on fixed rules or strategies learned through reinforcement learning (RL) that consider only a limited set of current features. To address this limitation, this paper introduces GCRL, an approach that enhances RL-based methods by integrating Graph Neural Networks (GNNs). GCRL encodes the history of LTS exploration into a graph structure, allowing it to capture a broader, non-current-based context. In a comparative experiment against state-of-the-art methods, GCRL exhibited superior learning efficiency and generalization across four out of five benchmark domains, except one particular domain characterized by high symmetry and strictly local interactions.