DSVA: An Iterative Refinement Multi-Agent Framework for NL-to-MTL Translation

Safety-critical cyber-physical systems require rigorously verifiable specifications, yet natural language (NL) requirements introduce ambiguity and defects. While Metric Temporal Logic (MTL) can express complex real-time constraints, manual NL-to-MTL translation is labor-intensive and error-prone. Existing single-agent LLM approaches like TR2MTL struggle with semantic ambiguity and lack automated refinement mechanisms. This paper proposes DSVA (Deconstruct-Synthesize-Verify-Analyze), a multi-agent framework with diagnostic-driven iterative refinement. DSVA deploys specialized agents: Deconstruct parses NL into semantic sketches; Synthesize generates MTL formulae; Verify controls iteration via back-translation and similarity checking; and Analyze diagnoses failures to guide refinement. A phase-specific Retrieval-Augmented Generation (RAG) mechanism enhances contextual understanding. Evaluation on the TR2MTL dataset across four LLMs shows DSVA achieves 85.6% mean accuracy, with GPT-4 reaching 90.9%, a 17.99 percentage point improvement over the TR2MTL baseline (72.91%). Comprehensive ablation studies reveal synergistic component interactions: RAG contributes + 15.1% when combined with iteration, iterative refinement contributes +14.4% when combined with RAG, yielding a + 7.6pp synergy bonus beyond additive effects (14.3pp<inline-formula> <tex-math notation="LaTeX">$\rightarrow 21.9$ </tex-math></inline-formula>pp). Even the weakest full DSVA configuration (Gemini-2.5-flash: 75.8%) surpasses the baseline. The framework&#x2019;s consistent cross-model performance gains validate its architectural benefits: specialized agent division of labor, automated iteration control, and diagnostic refinement, providing a potentially more reliable solution for automated requirements formalization in safety-critical systems.