ltlf2dfa 1.0.2

LTLf and PLTLf to Deterministic Finite-state Automata (DFA)

---

LTL_f2DFA 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:

• lark-parser 0.9.0
• sympy 1.6.1

They are automatically added while installing LTL_f2DFA.

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;
  • Pure-Past Linear Temporal Logic on Finite Traces.

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

NOTE: LTL_f2DFA 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_f2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).

Copyright 2018-2022 WhiteMech @ Sapienza University

Citing

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

Author

Francesco Fuggitti

History

1.0.2 (2022-02-25)

• Introduce PLTLfWeakBefore and PLTLfPastRelease support
• Hotfix problem on translation of the Once operator
• Increase code coverage

1.0.1 (2020-07-03)

• Introduce optional argument to to_dfa() method for DFA in MONA output
• Add parsing support for LTLfLast() and PLTLfStart() keywords
• Some fixes
• Increase code coverage

1.0.0.post0 (2020-06-05)

• Include *.lark files in the package build
• New online version: http://ltlf2dfa.diag.uniroma1.it/.

1.0.0 (2020-05-20)

• Refinement of all the grammars. Extensive improvement of the parsing.
• Introduce interfaces and class hierarchy for the logic modules.
• Several bug fixes and introduce testing.
• Introduce of docs.
• Introduce Continuous Integration.
• Refactor translation feature.
• Replace parsing library PLY with Lark.

0.2.2 (2019-09-25)

• Online version: http://ltlf2dfa.diag.uniroma1.it/.

0.2.0 (2019-09-03)

0.1.3 (2018-07-22)

0.1.0 (2018-07-18)

• First release on PyPI.