DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2019.17

Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions

Authors: Andrea Brunello, Angelo Montanari, and Mark Reynolds

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract

Linear temporal logic (LTL) is commonly used in model checking tasks; moreover, it is well-suited for the formalization of technical requirements. However, the correct specification and interpretation of temporal logic formulas require a strong mathematical background and can hardly be done by domain experts, who, instead, tend to rely on a natural language description of the intended system behaviour. In such situations, a system that is able to automatically translate English sentences into LTL formulas, and vice versa, would be of great help. While the task of rendering an LTL formula into a more readable English sentence may be carried out in a relatively easy way by properly parsing the formula, the converse is still an open problem, due to the inherent difficulty of interpreting free, natural language texts. Although several partial solutions have been proposed in the past, the literature still lacks a critical assessment of the work done. We address such a shortcoming, presenting the current state of the art for what concerns the English-to-LTL translation problem, and outlining some possible research directions.

Cite as

Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brunello_et_al:LIPIcs.TIME.2019.17,
  author =	{Brunello, Andrea and Montanari, Angelo and Reynolds, Mark},
  title =	{{Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.17},
  URN =		{urn:nbn:de:0030-drops-113756},
  doi =		{10.4230/LIPIcs.TIME.2019.17},
  annote =	{Keywords: Evolutionary algorithms, Machine learning, Natural language processing, Semantic parsing, Temporal logic}
}

Search Results

Documents authored by Brunello, Andrea

Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions

Abstract

Cite as

Thanks for your feedback!

Could not send message