This project aims to fix a common flaw in existing MATLAB ltl2ba(Linear Temporal Logic(LTL) to Büchi Automaton(BA)) packages where incorrect BA will be produced if the input LTL contains the logical connector not(aka. “¬”). This software will also provide some add-on functionalities such as producing Product Automaton(PA) and synthesizing a plan.
This software will be code in Python and will have the following functionality:
(1) Read input LTL formula and the environment modeled as Finite Transition System (FTS).
(2) Convert input LTL to BA through ltl2ba binary solver, provided by Denis Oddoux and Paul Gastin.
(3) Taking product of BA and FTS to form a PA. And these graphs can be visualized for helping debugging.
(4) Synthesize a plan based on input LTL formula and FTS.
Current status: Python part finished and tested. Next step would be developing a MATLAB wrapper for interacting with Python code through MATLAB.
Github Link: https://github.com/gaoqitong/LTL2FullProd