Skip to main content

From logic to automata.

Project description


PyPI PyPI - Python Version PyPI - Status PyPI - Implementation PyPI - Wheel GitHub

test lint docs codecov


LOGics formalisms to AUTomata

What is logaut

Logaut is to the logics-to-DFA problem what Keras is for Deep Learning: a wrapper to performant back-ends, but with human-friendly APIs.


To install the package from PyPI:

pip install logaut

Make sure to have Lydia installed on your machine. We suggest the following setup:

docker pull whitemech/lydia:latest
  • Make the Docker image executable under the name lydia. On Linux and MacOS machines, the following commands should work:
echo '#!/usr/bin/env sh' > lydia
echo 'docker run -v$(pwd):/home/default whitemech/lydia lydia "$@"' >> lydia
sudo chmod u+x lydia
sudo mv lydia /usr/local/bin/

This will install an alias to the inline Docker image execution in your system PATH. Instead of /usr/local/bin/ you may use another path which is still in the PATH variable.

On Windows, make a .bat file:

docker run --name lydia -v"%cd%":/home/default whitemech/lydia lydia %*

And add it to your PATH variable.


Now you are ready to go:

from logaut import ltl2dfa
from pylogics.parsers import parse_ltl
formula = parse_ltl("F(a)")
dfa = ltl2dfa(formula, backend="lydia")

The function ltl2dfa takes in input a pylogics formula and gives in output a pythomata DFA.

Then, you can manipulate the DFA as done with Pythomata, e.g. to print:


Currently, the lydia backend only supports the ltl and ldl logics.

The ltlf2dfa, based on LTLf2DFA, supports ltl and pltl. First, install it at version 1.0.1:

pip install git+

Then, you can use:

from logaut import pltl2dfa
from pylogics.parsers import parse_pltl
formula = parse_pltl("a S b")
dfa = pltl2dfa(formula, backend="ltlf2dfa")

Write your own backend

You can write your back-end by implementing the Backend interface:

from logaut.backends.base import Backend

class MyBackend(Backend):

    def ltl2dfa(self, formula: Formula) -> DFA:
        """From LTL to DFA."""

    def ldl2dfa(self, formula: Formula) -> DFA:
        """From LDL to DFA."""

    def pltl2dfa(self, formula: Formula) -> DFA:
        """From PLTL to DFA."""

    def pldl2dfa(self, formula: Formula) -> DFA:
        """From PLDL to DFA."""
    def fol2dfa(self, formula: Formula) -> DFA:
        """From FOL to DFA."""

    def mso2dfa(self, formula: Formula) -> DFA:
        """From MSO to DFA."""

Then, you can register the custom backend class in the library:

from logaut.backends import register
register(id_="my_backend", entry_point="")

And then, use it through the main entry point:

dfa = ltl2dfa(formula, backend="my_backend")


To run tests: tox

To run only the code tests: tox -e py3.7

To run only the linters:

  • tox -e flake8
  • tox -e mypy
  • tox -e black-check
  • tox -e isort-check

Please look at the tox.ini file for the full list of supported commands.


To build the docs: mkdocs build

To view documentation in a browser: mkdocs serve and then go to http://localhost:8000


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

Copyright 2021 WhiteMech


Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

logaut-0.2.0.tar.gz (19.3 kB view hashes)

Uploaded Source

Built Distribution

logaut-0.2.0-py3-none-any.whl (32.9 kB view hashes)

Uploaded Python 3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page