danielaisen / ltlf2dfa

From LTLf / PPLTL to Deterministic Finite-state Automata (DFA)

---

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.

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 .

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

If you want to contribute, set up your development environment as follows:

• Intall Poetry
• Clone the repository: git clone https://github.com/whitemech/LTLf2DFA.git && cd LTLf2DFA
• Install the dependencies: poetry shell && poetry install

Tests

To run tests: tox

To run only the code tests: tox -e py38

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_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