Automatic Syntax Error Repair for Discrete Controller Synthesis using Large Language Model

TL;DR

The paper tackles the bottleneck of syntax errors in Discrete Controller Synthesis (DCS) by developing a knowledge-informed Large Language Model (LLM) approach to automatically repair FSP/FLTL models. It derives an empirical error taxonomy from expert interviews and student workshops, and uses this domain knowledge to design prompts that guide corrections. A benchmark is built by injecting realistic errors into MTSA models, and the evaluation shows high repair accuracy, especially for grammar errors, with substantial practical benefits: roughly 3.46x faster fixes and a fraction of the cost compared to human debugging. The work demonstrates the viability of integrating LLM-based syntax repair into DCS workflows and points to future work on semantic repairs and tool integration within MTSA.

Abstract

Discrete Controller Synthesis (DCS) is a powerful formal method for automatically generating specifications of discrete event systems. However, its practical adoption is often hindered by the highly specialized nature of formal models written in languages such as FSP and FLTL. In practice, syntax errors in modeling frequently become an important bottleneck for developers-not only disrupting the workflow and reducing productivity, but also diverting attention from higher-level semantic design. To this end, this paper presents an automated approach that leverages Large Language Models (LLMs) to repair syntax errors in DCS models using a well-designed, knowledge-informed prompting strategy. Specifically, the prompting is derived from a systematic empirical study of common error patterns, identified through expert interviews and student workshops. It equips the LLM with DCS-specific domain knowledge, including formal grammar rules and illustrative examples, to guide accurate corrections. To evaluate our method, we constructed a new benchmark by systematically injecting realistic syntax errors into validated DCS models. The quantitative evaluation demonstrates the high effectiveness of the proposed approach in terms of repair accuracy and its practical utility regarding time, achieving a speedup of 3.46 times compared to human developers. The experimental replication suite, including the benchmark and prompts, is available at https://github.com/Uuusay1432/DCSModelRepair.git

Figures (9)

• Figure 1: Key Findings through Expert Interviews and Student Workshops.
• Figure 2: CM(2,2)
• Figure 3: CM(3,3)
• Figure 4: BW(2,2)
• Figure 5: BW(5,2)

Theorems & Definitions (1)

• Definition 1: Fluent Linear Temporal Logic (FLTL)