Signal Temporal Logic (STL) is widely used to specify timed and safety-critical tasks for cyber-physical systems, but writing STL formulas directly is difficult for non-expert users. Natural language (NL) provides a convenient interface, yet its inherent structural ambiguity makes one-to-one translation into STL unreliable. In this paper, we propose an \textit{ambiguity-preserving} method for translating NL task descriptions into STL candidate formulas. The key idea is to retain multiple plausible syntactic analyses instead of forcing a single interpretation at the parsing stage. To this end, we develop a three-stage pipeline based on Combinatory Categorial Grammar (CCG): ambiguity-preserving $n$-best parsing, STL-oriented template-based semantic composition, and canonicalization with score aggregation. The proposed method outputs a deduplicated set of STL candidates with plausibility scores, thereby explicitly representing multiple possible formal interpretations of an ambiguous instruction. In contrast to existing one-best NL-to-logic translation methods, the proposed approach is designed to preserve attachment and scope ambiguity. Case studies on representative task descriptions demonstrate that the method generates multiple STL candidates for genuinely ambiguous inputs while collapsing unambiguous or canonically equivalent derivations to a single STL formula.
翻译:信号时序逻辑(STL)广泛用于指定信息物理系统的时序和安全关键任务,但非专家用户难以直接编写STL公式。自然语言虽提供了便捷接口,但其固有的结构歧义使得一对一翻译为STL不可靠。本文提出一种保留歧义的方法,将自然语言任务描述翻译为STL候选公式。核心思想是在解析阶段保留多种合理的句法分析结果,而非强制选择单一解释。为此,我们基于组合范畴语法开发了三阶段流水线:保留歧义的n-best解析、面向STL的模板化语义组合、以及结合分数聚合的规范化处理。该方法输出带合理度分数的去重STL候选集,从而显式表示歧义指令的多种可能形式化解释。与现有单候选自然语言到逻辑翻译方法不同,本文方法专门设计用于保留附着和辖域歧义。对代表性任务描述的案例研究表明,该方法能为真正歧义的输入生成多个STL候选,同时将无歧义或规范等价的推导结果合并为单一STL公式。