Towards Explainable Formal Methods: from LTL to Natural Language with Neural Machine TranslationResearch Preview
[Context and motivation] Requirements formalization facilitates reasoning about inconsistencies, detection of ambiguities, and identification of critical issues in system models. Temporal logic formulae are the natural choice when it comes to formalizing requirements associated with desired system behaviours. [Question/problem] Understanding and mastering temporal logic require a formal background. Means are therefore needed to make temporal logic formulae interpretable by engineers, domain experts, and other stakeholders involved in the development process. [Principal ideas/results] In this paper, we propose to use a neural machine translation tool, named OpenNMT, to translate Linear Temporal Logic (LTL) formulae into corresponding natural language descriptions. Our results show that our translation system achieves an average BLEU (BiLingual Evaluation Understudy) score of 78%, which corresponds to high-quality translations. [Contribution] Our neural model can be applied to assess if requirements have been correctly formalized. This can be useful to requirements analysts, who may have limited confidence with LTL, and to other stakeholders involved in the requirements verification process. Overall, our work contributes to bridging the gap between formal methods and requirements engineering and opens to further research in explainable formal methods.