ltlf2dfa 0.2.0.post3

A tool for generating a DFA from an LTLf formula

LTL_f2DFA

LTL_f2DFA is a simple tool that processes an LTL_f formula (with past or future operators) and generates the corresponding minimized DFA (Deterministic Finite state Automaton) using MONA. This tool is written in Python 3.6.

It is tested on Linux Ubuntu 16.04 and on macOS 10.13.6.

Now it is also available online at ltlf2dfa.diag.uniroma1.it.

Getting Started

Requirements

This tool uses MONA for the generation of the DFA. Hence, you should first install MONA with all its dependencies on your OS following the instructions here.

This tool is also based on the following libraries:

• ply 3.11
• graphviz 0.8.3
• dotpy 0.0.2

They are automatically added while installing LTL_f2DFA.

How To Install It

• From PyPI:

pip install ltlf2dfa

• From this repository:

pip install git+https://github.com/Francesco17/LTLf2DFA@distribution#egg=ltlf2dfa

How To Use It

• Simply parse an LTL_f formula with past or future operators:

from ltlf2dfa.Parser import MyParser

formula = "G(a->Xb)"
parser = MyParser()
parsed_formula = parser(formula)

print(parsed_formula)

• Translate an LTL_f formula to the corresponding DFA automaton:

from ltlf2dfa.Translator import Translator
from ltlf2dfa.DotHandler import DotHandler

formula = "G(a->Xb)"
declare_flag = False #True if you want to compute DECLARE assumption for the formula

translator = Translator(formula)
translator.formula_parser()
translator.translate()
translator.createMonafile(declare_flag) #it creates automa.mona file
translator.invoke_mona() #it returns an intermediate automa.dot file

dotHandler = DotHandler()
dotHandler.modify_dot()
dotHandler.output_dot() #it returns the final automa.dot file

Syntax

The syntax accepted by LTL_f2DFA is the following:

OPERATOR	SYMBOL
TRUE	T
FALSE	F
AND	&
OR	|
NOT	~
IMPLICATION	->
D-IMPLICATION	<->
NEXT	X
UNTIL	U
EVENTUALLY	E
GLOBALLY	G
YESTERDAY (*)	Y
SINCE (*)	S
ONCE (*)	O
GLOBALLY (*)	H

(*) are PAST operators.

Also parentheses ( and ) can be used.

NOTE: LTL_f2DFA accepts ONLY separated formulas, i.e. formulas that have only past, only future or none operators.

Author

Francesco Fuggitti

License

This project is licensed under the MIT License - see the LICENSE file for details

Contacts

If, for any reason, you are interested in feel free to contact me by email.