Towards Efficient Discrete Controller Synthesis: Semantics-Aware Stepwise Policy Design via LLM

Discrete Controller Synthesis (DCS) is an automated generation technique to generate controllers from environment models and requirements. The time and space complexities of DCS are critical because they directly govern the feasibility of using DCS for real-time generation of controllers to cope with environmental changes. Stepwise DCS is considered a promising approach to prevent the construction of ineffective state spaces in the subsequent analysis of the full controller by analyzing sub-controllers that meet part of the requirements at an early stage. However, constructing a stepwise policy is a challenge, as the current methods often require domain experts to manually build it by understanding and reasoning the semantics of each sub-environment model and sub-requirement. To reduce the effort of manual construction, this paper introduces a method that leverages large language models (LLMs) to automate the generation of stepwise policies by utilizing the LLM's ability to understand and reason about the semantics of state machines. The evaluation using GPT-4 on a drone control scenario demonstrates the effectiveness of our method, with an average reduction of 82.2% in states and 91.2% in transitions.