search

RiccardoDeMasellis / FLLOAT

A library for generating automata from LTL and LDL formulas with finite-trace semantics.
11 stars 1 forks source link

Project Alive? #10

Closed digitalw closed 6 years ago

digitalw commented 6 years ago

Hi, Is this Project still alive?

RiccardoDeMasellis commented 6 years ago

We believe it works by doing what is written in the description. So we are not actively working on it, if this is what you mean.

digitalw commented 6 years ago

I was wondering about the performance improvements worked on in the optimizations branch :-)

RiccardoDeMasellis commented 6 years ago

I am not working on it, as in general the optimization I had in mind does not work.

However, for input formulas with a specific "structure", it is possible to speed up the process of automata generation. In particular if you have a boolean combination of temporal formulas, instead of building the automaton for the whole formula, you can build the automata for the temporal (sub-)formulas, minimize them and then combine the resulting automata together using the well-known operations on automata.

digitalw commented 6 years ago

Thanks for the hint. I will give it a try.

RiccardoDeMasellis commented 6 years ago

The general problem is that the procedure does not generate minimal automata, which kills the performances. So, if you can (but that depends on your input formulas) is better to: (i) push inside the temporal operators; (ii) use the automaton construction procedure in the temporal sub-formulas; (iii) minimize the resulting automata and finally (iv) re-combine them with the automata operations (intersection for and, union for or and negation for not).