GenCTL: Constraint-Guided LLM Generation of Verifiable CTL Specifications from Natural Language Requirements

Abstract

Natural language (NL) requirements are widely used in system design, but their ambiguity makes formal verification difficult. Translating NL requirements into Computation Tree Logic (CTL) is challenging because generated formulas must be both semantically appropriate and compatible with concrete verification models. Although large language models (LLMs) provide a promising basis for NL-to-CTL(NL2CTL) translation, their outputs are often unstable and prone to parsing, typing, and grounding errors. To address these issues, we propose GenCTL, a prompt-based framework for effective and model-aware NL2CTL translation without task-specific fine-tuning. GenCTL combines structured prompting, retrieval-enhanced few-shot examples, atomic-proposition (AP) grounding from nuXmv models, multi-candidate generation with frequency-first selection and length-normalized log-likelihood tie-breaking, and interactive refinement through an explanation dictionary. Experimental results demonstrate the effectiveness of the proposed framework in both model-agnostic and model-aware settings. On a generated NL--CTL dataset, the best automatically selected translation achieves 68% accuracy, which increases to 92% after one round of user refinement. On 150 NL requirements grounded in three nuXmv models, AP-list prompting yields 139/150 directly checkable formulas, increasing to 149/150 after lightweight normalization. These results show that GenCTL improves the reliability and practical checkability of LLM-generated CTL specifications.