About

DFA games is a software for solving games over a Deterministic Finite-state Automaton (DFA). Here, the DFA is defined using Linear Temporal Logic interpreted over finite traces with either past or future operators. The tool prints the DFA corresponding to the formula and colors its nodes according to the following criteria:
(i) nodes NOT belonging to the winning set are gray
(ii) colors nodes in the winning set range from light-blue, for the final state; to yellow, for the most distant states (where colors are ordered according to their frequency and states according to the number of worst-case steps to reach the final state).

Acknowledgments

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

References
  • 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.
  • 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.
  • 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
  • LTL and Past LTL on Finite Traces for Planning and Declarative Process Mining
    Fuggitti F.
    In M.Sc. Thesis. Sapienza University of Rome, 2018