About

LTLf2DFA is a tool that transforms an LTLf or a PLTLf formula into a minimal Deterministic Finite state Automaton (DFA) using MONA. The resulting DFA is symbolic in the transitions.

Citing

If you are interested in this tool, and you use it in your own work, please consider citing it.
DOI

License

LTLf2DFA is licensed under the GNU Lesser General Public License v3 or later License (LGPLv3+).

Author

LTLf2DFA is developed and maintained by Francesco Fuggitti.

Acknowledgments

This project (© 2018-) is proudly funded by the WhiteMech ERC AG no.834228 under the European Union's Horizon 2020 research and innovation programme.

References
  • Pure-Past Linear Temporal and Dynamic Logic on Finite Traces
    De Giacomo, G.; Di Stasio, A.; Fuggitti, F.; Rubin, S.
    In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, (IJCAI), Survey Track, 2020.
  • First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
    Zhu, S.; Pu, G.; Vardi, M. Y.
    In Theory and Applications of Models of Computation. TAMC 2019. Lecture Notes in Computer Science. Springer, 2019.
  • LTL and Past LTL on Finite Traces for Planning and Declarative Process Mining
    Fuggitti F.
    In M.Sc. Thesis. Sapienza University of Rome, 2018
  • Linear Temporal Logic and Linear Dynamic Logic on Finite Traces
    De Giacomo, G. and Vardi, M. Y.
    In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI), 2013.
  • MONA Version 1.4 User Manual
    Klarlund, N. and Møller, A.
    In Notes Series NS-01-1. BRICS, Department of Computer Science, University of Aarhus, 2001