一句话：提出交互式工具 TLCrafter，用 LLM 分解与规则合成将自然语言需求翻译为 LTL/CTL/STL 时序逻辑公式。
自然语言需求在工业系统中广泛使用，但形式验证通常需要精确的时序逻辑规约。本文提出交互式工具 TLCrafter，将自然语言需求翻译为 LTL、CTL 和 STL 公式。该工具构建 OnionL+ 分层中间表示，将基于 LLM 的语义分解与确定性的规则合成相结合，以提高 NL-to-TL 形式化的鲁棒性；其可视化界面允许工程师在公式生成前检查并修正中间结构。在跨 LTL、CTL 和 STL 的领域数据集上，实验表明 TLCrafter 在保持公式完全语法有效性的同时提升了准确率。
Natural-language (NL) requirements are widely used in industrial systems, but formal verification typically requires precise temporal logic (TL) specifications. This paper presents TLCrafter, an interactive tool for translating NL requirements into TL formulas, including LTL, CTL, and STL. Given an NL requirement, TLCrafter constructs OnionL+, a hierarchical intermediate representation that supports more robust NL-to-TL formalization by combining LLM-based semantic decomposition with deterministic rule-based synthesis. Its visual interface allows engineers to inspect and correct the intermediate structure before formula generation. Experiments on domain datasets across LTL, CTL, and STL show that TLCrafter improves formula accuracy while maintaining full syntactic validity. A video of TLCrafter is available at https://youtu.be/jp-Pp_amjks. The tool and artifacts are available at https://sites.google.com/view/tlcrafter/.
@inproceedings{paperbot12436,
title = {TLCrafter: Peeling the Layers of Natural Language to Reveal Temporal Logic Specifications},
author = {Cheng Wen and Wenjun Ke and Xiao Liang and Zhi Ma and Xiaoyong Xue and Shengchao Qin and Cong Tian},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834598}
}