LTL_f2DFA is a tool that transforms an LTL_f or a PPLTL formula into a minimal Deterministic Finite state Automaton (DFA) using MONA.

It is also available online at http://ltlf2dfa.diag.uniroma1.it.

Prerequisites

MONA Installation

LTL_f2DFA relies on the MONA tool for the generation of the DFA. Please, make sure you have the MONA tool installed on your system before running LTL_f2DFA. You can follow the instructions here to get MONA.

Installation

Install the latest release from PyPI:

pip install ltlf2dfa

When using uv in another Python project:

uv add ltlf2dfa

Install the latest development version from GitHub:

pip install git+https://github.com/whitemech/LTLf2DFA.git

Alternatively, clone the repository:

git clone https://github.com/whitemech/LTLf2DFA.git
cd LTLf2DFA
uv sync

Quickstart

You can use the LTL_f2DFA package in two ways: as a library, and as a CLI tool.

As a Library

• 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 PPLTL formula:

from ltlf2dfa.parser.ppltl import PPLTLParser

parser = PPLTLParser()
formula_str = "H(a -> Y b)"
formula = parser(formula_str)  # returns a PPLTLFormula

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

As a CLI Interface

ltlf2dfa -l {ltlf | ppltl} -f <path/to/formula>

Features

• Syntax and parsing support for the following formal languages:

  • Propositional Logic;
  • Linear Temporal Logic on Finite Traces;
  • Pure-Past Linear Temporal Logic on Finite Traces.

• Conversion from LTL_f/PPLTL formula to MONA (First-order Logic)

NOTE: LTL_f2DFA accepts either LTL_f formulas or PPLTL formulas, i.e., formulas that have only past, only future or none operators.

Development

Requirements

To work on LTLf2DFA, you need:

• Python 3.11 or later
• uv
• MONA

Clone the repository and synchronize the development environment:

git clone https://github.com/whitemech/LTLf2DFA.git
cd LTLf2DFA
uv sync

There is no need to activate the virtual environment manually. Project commands can be run with uv run.

Tests

Run the complete test suite:

uv run pytest

Run tests with coverage:

uv run pytest \
  --cov=ltlf2dfa \
  --cov-report=term-missing \
  --cov-report=xml

Code quality

Check the code with Ruff:

uv run ruff check .
uv run ruff format --check .

Apply automatic linting and formatting fixes:

uv run ruff check . --fix
uv run ruff format .

Pre-commit hooks

Install the Git pre-commit hooks:

uv run pre-commit install

Run all hooks manually:

uv run pre-commit run --all-files

Documentation

Build the documentation:

uv run mkdocs build --clean --strict

Serve the documentation locally:

uv run mkdocs serve

Then open http://localhost:8000 in your browser.

Build

Build the source distribution and wheel:

uv build

The generated artifacts are written to the dist/ directory.

License

LTL_f2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).

Copyright 2018-2023 WhiteMech

Citing

If you use LTL_f2DFA in your research, please consider citing it with the following bibtex:

@software{fuggitti-ltlf2dfa,
  author       = {Francesco Fuggitti},
  title        = {LTLf2DFA},
  month        = {March},
  year         = {2019},
  publisher    = {Zenodo},
  version      = {1.0.3},
  doi          = {10.5281/zenodo.3888410},
  url_code    = {https://github.com/whitemech/LTLf2DFA},
  url_website = {http://ltlf2dfa.diag.uniroma1.it},
}

Author

Francesco Fuggitti