Elamur Research⌕
☰
home / papers / 2021 / DeepSTL — From English Requirements to Signal Temporal Logic

DeepSTL — From English Requirements to Signal Temporal Logic

Paper · 2021 · Jie He, Ezio Bartocci, Dejan Ničkovic et al.

Summary

The paper addresses a practical barrier to formal methods: engineers find it hard to turn natural-language requirements for cyber-physical systems into Signal Temporal Logic (STL). STL extends LTL with timed operators over real-valued, dense-time signals. Learning such a translator is difficult because public pairs of informal requirements and formal specifications are almost nonexistent.

The authors work around this in two stages. First, they analyse which STL constructs actually occur in the scientific literature. They use those statistics to drive a grammar-based generator that samples STL formulas and renders each one into several English phrasings. Second, they train a transformer to map English to STL and compare it with attentional and plain seq2seq baselines.

The transformer translates requirement patterns that are well represented in training with high quality. Accuracy falls on requirements that differ strongly from the synthetic data. The work shows that synthetic corpora generated from the formal side can bootstrap semantic parsing into a logic when no real data exists.

Key points

  • Tool and venue: DeepSTL was published at ICSE '22. Code is at github.com/JieHE-2020/DeepSTL, and the artifact DOI is 10.6084/m9.figshare.19091282.
  • Research questions: five in total.
    • RQ1–RQ2 cover the data shortage: STL usage statistics from the literature and synthetic generation that matches them.
    • RQ3–RQ5 cover translation: learning synthetic STL, extrapolating to literature requirements, and comparing architectures.
  • Target logic: an STL variant that combines operators looking into the past with operators looking into the future. This includes always and eventually with time intervals, since, until, once, historically, and rise/fall edge operators.
  • Baseline comparison: Att-seq2seq comes close to the Transformer but makes meaning-reversing mistakes, such as inserting a negation. Plain Seq2seq does not even recover the formula template.
  • Error analysis: the models learn statistical patterns rather than meaning, as shown by "greater than" becoming "<". The authors also note that their template-accuracy metric unfairly over-penalises positional shifts.

Interesting ideas

  • I1. Build training pairs from the formal side by sampling a logical formula and rendering many English paraphrases from a grammar, so no human annotation is needed.
  • I2. Weight the synthetic generator by how often constructs appear in real specifications, rather than sampling uniformly. This keeps the corpus focused on patterns people actually write.
  • I3. Separate structural ("template") accuracy from slot-filling accuracy, while making sure the structural metric does not over-punish shifted positions.
  • I4. Read decoder confidence as a diagnostic: low confidence suggests undertrained features, but high confidence can still hide a stubbornly wrong output.
  • I5. Map phrases like "whenever X then within 100 units Y holds for 20 units" onto a small set of timed operators (always, eventually, rise, fall) with explicit intervals.

For Mova

How these ideas could serve Mova, our small open language model — its files, stages and tests:

  • I1 (learn): sample frame structures and render them through the back generator to create silver sentence/frame pairs for training and stress-testing frame extraction.
  • I2 (learn): bias synthetic frame and tree generation by construction frequencies counted in the treebanks, so silver data matches real usage.
  • I3 (learn): score frame graphs separately on skeleton and on argument fillers, using alignment-based matching instead of position-by-position comparison.
  • I4 (learn): log parser confidence per construction to find gaps in the training data, and pair it with negative controls so confident errors are still caught.
  • I5 (world): use such bounded temporal operators to represent event order and durations in the text's world, so timing questions can be checked explicitly.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓TU WienVienna · Austria5 works · 757 citations🔬AIT Austrian Institute of Technology GmbHVienna · Austria2 works · 239 citations

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 9,086 worksArtificial Intelligence · 8,889 worksComputational Theory and Mathematics · 116 worksSoftware · 25 works

Cite

Cite as Jie He, Ezio Bartocci, Dejan Ničkovic, Haris Isakovic and Radu Grosu. 2021. DeepSTL — From English Requirements to Signal Temporal Logic. arXiv:2109.10294.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2109.10294 · arXiv 2109.10294

@misc{he2021deepstl,
  title = {{DeepSTL — From English Requirements to Signal Temporal Logic}},
  author = {Jie He, Ezio Bartocci, Dejan Nivckovic, Haris Isakovic and Radu Grosu},
  year = {2021},
  doi = {10.48550/arxiv.2109.10294},
  eprint = {2109.10294},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2109.10294}
}

References

60 references, 13 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan. Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification, pages 135–175. Springer, 2018. find
  2. Oded Maler and Dejan Ničković. Monitoring properties of analog and mixed-signal circuits. International Journal on Software Tools for Technology Transfer, 15(3):247–268, 2013. ↗
  3. Rani Nelken and Nissim Francez. Automatic translation of natural language system specifications. In Proc. of CAV’96: the 8th International Conference on Computer Aided Verification, volume 1102 of LNCS, pages 360–371. Springer, 1996. find
  4. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In Proc. of ICSE’ 99: the 1999 International Conference on Software Engineering, pages 411–420. ACM, 1999. find
  5. Aarne Ranta. Translating between language and logic: What is easy and what is difficult. In Proc. of CADE-23: the 23rd International Conference on Automated Deduction, volume 6803 of LNCS, pages 5–25. Springer, 2011. find
  6. Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. Translating structured english to robot controllers. Adv. Robotics, 22(12):1343–1359, 2008. ↗
  7. Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. Formal consistency checking over specifications in natural languages. In Proc. of DATE 2015: the 2015 Design, Automation & Test in Europe, pages 1677–1682. ACM, 2015. ↗
  8. Marco Autili, Lars Grunske, Markus Lumpe, Patrizio Pelliccione, and Antony Tang. Aligning qualitative, real-time, and probabilistic property specification patterns using a structured english grammar. IEEE Trans. Software Eng., 41(7):620– 638, 2015. ↗
  9. Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of LTL formulas from natural language texts: State of the art and research directions. In Proc. of TIME 2019: the 26th International Symposium on Temporal Representation and Reasoning, volume 147 of LIPIcs, pages 17:1–17:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. ↗
  10. Allen P. Nikora and Galen Balcom. Automated identification of LTL patterns in natural language requirements. In Proc. of ISSRE 2009: the 20th International Symposium on Software Reliability Engineering, pages 185–194, 2009. find
  11. Constantine Lignos, Vasumathi Raman, Cameron Finucane, Mitchell P. Marcus, and Hadas Kress-Gazit. Provably correct reactive control from natural language. Auton. Robots, 38(1):89–105, 2015. ↗
  12. Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. Formal consistency checking over specifications in natural languages. In Proc. of 2015 Design, Automation Test in Europe Conference Exhibition (DATE), pages 1677–1682. IEEE, 2015. ↗
  13. Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. ARSENAL: automatic requirements specification extraction from natural language. In Proc. of NFM 2016: the 8th International Symposium on NASA Formal Methods, volume 9690 of LNCS, pages 41–46. Springer, 2016. find
  14. Alessandro Fantechi, Stefania Gnesi, Gioia Ristori, Michele Carenini, Massimo Vanocchi, and Paolo Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods Syst. Des., 4(3):243–263, 1994. ↗
  15. Juraj Dzifcak, Matthias Scheutz, Chitta Baral, and Paul Schermerhorn. What to do and how to do it: Translating natural language directives into temporal and dynamic logic representation for goal management and action execution. In Proc. of ICRA 2009: the IEEE International Conference on Robotics and Automation, pages 4163–4168, 2009. find
  16. Christopher B. Harris and Ian G. Harris. Generating formal hardware verification properties from natural language documentation. In Proceedings of the 2015 IEEE 9th International Conference on Semantic Computing (IEEE ICSC 2015), pages 49–56, 2015. find
  17. Sascha Konrad and Betty H. C. Cheng. Real-time specification patterns. In Proc. of ICSE: the 27th International Conference on Software Engineering, ICSE ’05, page 372–381, New York, NY, USA, 2005. ACM. find
  18. Tainã Santos, Gustavo Carvalho, and Augusto Sampaio. Formal modelling of environment restrictions from natural-language requirements. In Proc. of SBMF 2018: the 21st Brazilian Symposium on Formal Methods: Foundations and Applications, volume 11254 of LNCS, pages 252–270. Springer, 2018. find
  19. Amir Pnueli. The temporal logic of programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science, pages 46–57. IEEE, 1977. find
  20. Chaima Boufaied, Maris Jukss, Domenico Bianculli, Lionel Claude Briand, and Yago Isasi Parache. Signal-based properties of cyber-physical systems: Taxonomy and logic-based characterization. Journal of Systems and Software, 174:110881, 2021. ↗
  21. Bardh Hoxha, Houssam Abbas, and Georgios E. Fainekos. Benchmarks for temporal logic requirements for automotive systems. In Goran Frehse and Matthias Althoff, editors, Proc. of ARCH@CPSWeek 2014/15: the 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, volume 34 of EPiC Series in Computing, pages 25–30. EasyChair, 2014. find
  22. Yuk Wah Wong and Raymond J. Mooney. Learning for semantic parsing with statistical machine translation. In Robert C. Moore, Jeff A. Bilmes, Jennifer Chu-Carroll, and Mark Sanderson, editors, Proc. of Human Language Technology Conference of the North American Chapter of the Association of Computational Linguistics. The Association for Computational Linguistics, 2006.
  23. Sempre: Semantic parsing with execution, Accessed 2021. find
  24. Rohit J. Kate and Raymond J. Mooney. Using string-kernels for learning semantic parsers. In Nicoletta Calzolari, Claire Cardie, and Pierre Isabelle, editors, Proc. of ACL 2006: the 21st International Conference on Computational Linguistics and 44th Annual Meeting of the Association for Computational Linguistics. The Association for Computer Linguistics, 2006.
  25. Sippycup, Accessed 2021. find
  26. Yoav Artzi. Cornell SPF: Cornell semantic parsing framework, 2016. find
  27. Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, and Thomas Dillig. Sqlizer: query synthesis from natural language. Proc. ACM Program. Lang., 1(OOPSLA):63:1– 63:26, 2017. ↗
  28. Fei Li and H. V. Jagadish. Constructing an interactive natural language interface for relational databases. Proc. VLDB Endow., 8(1):73—-84, September 2014. ↗
  29. Lappoon R. Tang and Raymond J. Mooney. Automated construction of database interfaces: Intergrating statistical and relational learning for semantic parsing. In Proc. of 2000 Joint SIGDAT Conference on Empirical Methods in Natural Language Processing and Very Large Corpora, pages 133–141. Association for Computational Linguistics, 2000. find
  30. John M. Zelle and Raymond J. Mooney. Learning to parse database queries using inductive logic programming. In Proc. of AAAI 96, IAAI 96:the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, pages 1050–1055. AAAI Press / The MIT Press, 1996.
  31. Victor Zhong, Caiming Xiong, and Richard Socher. Seq2sql: Generating structured queries from natural language using reinforcement learning. CoRR, abs/1709.00103, 2017. ↗
  32. Yusuke Oda, Hiroyuki Fudaba, Graham Neubig, Hideaki Hata, Sakriani Sakti, Tomoki Toda, and Satoshi Nakamura. Learning to generate pseudo-code from source code using statistical machine translation (T). In Myra B. Cohen, Lars Grunske, and Michael Whalen, editors, Proc. of ASE 2015: the 30th IEEE/ACM International Conference on Automated Software Engineering, pages 574–584. IEEE Computer Society, 2015. find
  33. Xi Victoria Lin, Chenglong Wang, Luke Zettlemoyer, and Michael D. Ernst. NL2Bash: A corpus and semantic parser for natural language interface to the linux operating system. In Nicoletta Calzolari, Khalid Choukri, Christopher Cieri, Thierry Declerck, Sara Goggi, Kôiti Hasida, Hitoshi Isahara, Bente Maegaard, Joseph Mariani, Hélène Mazo, Asunción Moreno, Jan Odijk, Stelios Piperidis, and Takenobu Tokunaga, editors, Proc. of LREC 2018: the Eleventh International Conference on Language Resources and Evaluation. European Language Resources Association (ELRA), 2018. find
  34. Chris Quirk, Raymond Mooney, and Michel Galley. Language to code: Learning semantic parsers for if-this-then-that recipes. In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 1: Long Papers), pages 878–888, Beijing, China, 2015. Association for Computational Linguistics. find
  35. Nikhil Ketkar. Introduction to PyTorch, pages 195–208. Apress, Berkeley, CA, 2017. find
  36. Martín Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek Gordon Murray, Benoit Steiner, Paul A. Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. Tensorflow: A system for large-scale machine learning. In Proc. of OSDI 2016: the 12th USENIX Symposium on Operating Systems Design and Implementation, pages 265–283. USENIX Association, 2016. ↗
  37. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, pages 5998–6008, 2017.
  38. Xiaoqing Jin, Jyotirmoy V Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. Powertrain control verification benchmark. In Proceedings of the 17th international conference on Hybrid systems: computation and control, pages 253– 262, 2014. find
  39. Christoph Gladisch, Thomas Heinz, Christian Heinzemann, Jens Oehlerking, Anne von Vietinghoff, and Tim Pfitzer. Experience paper: Search-based testing in automated driving control applications. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 26–37. IEEE, 2019. find
  40. Zhiyu Liu, Bo Wu, Jin Dai, and Hai Lin. Distributed communication-aware motion planning for multi-agent systems from stl and spatel specifications. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pages 4452–4457. IEEE, 2017. find
  41. Parv Kapoor, Anand Balakrishnan, and Jyotirmoy V Deshmukh. Model-based reinforcement learning from signal temporal logic specifications. arXiv preprint arXiv:2011.04950, 2020. ↗
  42. Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), pages 6565–6570. IEEE, 2016. find
  43. Hsuan-Cheng Liao. A survey of reinforcement learning with temporal logic rewards, 2020. ↗
  44. Wenliang Liu and Calin Belta. Model-based safe policy search from signal temporal logic specifications using recurrent neural networks. arXiv preprint arXiv:2103.15938, 2021. ↗
  45. Gang Chen, Mei Liu, and Zhaodan Kong. Temporal-logic-based semantic fault diagnosis with time-series data from industrial internet of things. IEEE Transactions on Industrial Electronics, 68(5):4393–4403, 2020. ↗
  46. Infineon datasheet. https://www.infineon.com/dgdl/Infineon-BTS5016-2EKA-DS-v01_00-EN.pdf?fileId=5546d4625a888733015aa41a5e161129. ↗
  47. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. In Advances in neural information processing systems, pages 3104–3112, 2014. ↗
  48. Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning to align and translate. arXiv preprint arXiv:1409.0473, 2014. ↗
  49. Jiatao Gu, Zhengdong Lu, Hang Li, and Victor O.K. Li. Incorporating copying mechanism in sequence-to-sequence learning. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1631–1640. Association for Computational Linguistics, 2016.
  50. Rico Sennrich, Barry Haddow, and Alexandra Birch. Neural machine translation of rare words with subword units. In Proc. of ACL 2016: the 54th Annual Meeting of the Association for Computational, Volume 1: Long Papers, 2016.
  51. Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, Nishant Patil, Wei Wang, Cliff Young, Jason Smith, Jason Riesa, Alex Rudnick, Oriol Vinyals, Greg Corrado, Macduff Hughes, and Jeffrey Dean. Google’s neural machine translation system: Bridging the gap between human and machine translation. CoRR, abs/1609.08144, 2016. ↗
  52. Taku Kudo. Subword regularization: Improving neural network translation models with multiple subword candidates. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 66–75, Melbourne, Australia, July 2018. Association for Computational Linguistics.
  53. Aston Zhang, Zachary C Lipton, Mu Li, and Alexander J Smola. Dive into deep learning. arXiv preprint arXiv:2106.11342, 2021. ↗
  54. Kyunghyun Cho, Bart Van Merriënboer, Dzmitry Bahdanau, and Yoshua Bengio. On the properties of neural machine translation: Encoder-decoder approaches. arXiv preprint arXiv:1409.1259, 2014. ↗
  55. Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014. ↗
  56. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002.
  57. Steven Y Feng, Varun Gangal, Jason Wei, Sarath Chandar, Soroush Vosoughi, Teruko Mitamura, and Eduard Hovy. A survey of data augmentation approaches for NLP. arXiv preprint arXiv:2105.03075, 2021. ↗
  58. Jing Li, Aixin Sun, Jianglei Han, and Chenliang Li. A survey on deep learning for named entity recognition. IEEE Transactions on Knowledge and Data Engineering, 34(1):50–70, 2020. ↗
  59. Vikas Yadav and Steven Bethard. A survey on recent advances in named entity recognition from deep learning models. arXiv preprint arXiv:1910.11470, 2019. ↗
  60. Xipeng Qiu, Tianxiang Sun, Yige Xu, Yunfan Shao, Ning Dai, and Xuanjing Huang. Pre-trained models for natural language processing: A survey. Science China Technological Sciences, 63(10):1872–1897, 2020. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/he-2021-deepstl-english-requirements-signal-temporal/