一句话：分析LTL规格形式化错误，发现语言学现象可解释近半新手与多数专家错误。
形式化方法的关键挑战之一是将自然语言需求准确形式化；错误的形式化可能漏掉缺陷，甚至将缺陷存在性固化下来。已有研究表明，即使是经验丰富的专家，在将相对简单的规格形式化为线性时序逻辑（LTL）时也会犯错。本文从“为语句增添额外意义的语言学现象”这一视角，重新分析一项近期研究的数据，考察对这类现象是否以及何时应被形式化的误解如何影响错误。结果发现，此类误解可能影响数据集中近一半的新手错误以及大多数专家错误。作者据此认为，进一步研究自然语言规格与这些具体语言现象之间的关系，有潜力减少误形式化。
One of the key challenges in using formal methods is producing accurate formalizations of natural language requirements, as providing incorrect formalizations may miss bugs or even codify their existence. Yet despite this critical role, recent studies have revealed that even experienced experts make mistakes when formalizing relatively simple specifications in Linear Temporal Logic (LTL). We analyze the data from one recent study from the perspective of linguistic phenomena that enrich what is said with additional meaning. We find that misunderstanding whether and when to formalize these phenomena could impact nearly half of novice mistakes and most expert mistakes in the dataset. We conclude that further study of the relationship between natural language specifications and these specific phenomena has potential to reduce misformalizations.
DOI 原文 ·
@inproceedings{paperbot9375,
title = {Linguistic Theories Coincide with Misformalization in Temporal Logic},
author = {Colin S. Gordon},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00329}
}