LTL_{f}2DFA is a tool that transforms an LTL_{f} or a PLTL_{f} formula into a minimal Deterministic Finite state Automaton (DFA) using MONA.
It is also available online at http://ltlf2dfa.diag.uniroma1.it.
Prerequisites
This tool uses MONA for the generation of the DFA. Hence, you should first install MONA with all its dependencies on your system following the instructions here.
This tool is also based on the following libraries:
They are automatically added while installing LTL_{f}2DFA.
Install
 from PyPI:
pip install ltlf2dfa

or, from source (
master
branch):pip install git+https://github.com/whitemech/LTLf2DFA.git

or, clone the repository and install:
git clone https://github.com/whitemech/LTLf2DFA.git cd ltlf2dfa pip install .
How To Use
 Parse an LTL_{f} formula:
from ltlf2dfa.parser.ltlf import LTLfParser parser = LTLfParser() formula_str = "G(a > X b)" formula = parser(formula_str) # returns an LTLfFormula print(formula) # prints "G(a > X (b))"
 Or, parse a PLTL_{f} formula:
from ltlf2dfa.parser.pltlf import PLTLfParser parser = PLTLfParser() formula_str = "H(a > Y b)" formula = parser(formula_str) # returns a PLTLfFormula print(formula) # prints "H(a > Y (b))"
 Translate a formula to the corresponding DFA automaton:
dfa = formula.to_dfa() print(dfa) # prints the DFA in DOT format
Features

Syntax and parsing support for the following formal languages:
 Propositional Logic;
 Linear Temporal Logic on Finite Traces;
 PurePast Linear Temporal Logic on Finite Traces.

Conversion from LTL_{f}/PLTL_{f} formula to MONA (Firstorder Logic)
NOTE: LTL_{f}2DFA accepts either LTL_{f} formulas or PLTL_{f} formulas, i.e., formulas that have only past, only future or none operators.
Tests
To run tests: tox
To run only the code tests: tox e py3.7
To run only the code style checks: tox e flake8
Docs
To build the docs: mkdocs build
To view documentation in a browser: mkdocs serve
and then go to http://localhost:8000
License
LTL_{f}2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).
Copyright 20182020 WhiteMech @ Sapienza University
Citing
If you are interested in this tool, and you use it in your own work, please consider citing it.