Linguistic Theories Coincide with Misformalization in Temporal Logic

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.