Hi Homer!

"Walke, Homer" homer_walke@brown.edu writes:

I know Spot doesn't provide much support for LTLf (LTL with finite trace semantics) but I need to simplify some LTLf formulas. I was wondering which tl_simplifier_options, if any, would simplify according to the semantics of LTLf, i.e reduce_basics, synt_impl, etc. I know that using all the rewritings wouldn't work since many of them only apply to LTL and not LTLf but I'd like to use any rewritings that do apply to LTLf.

All those rewritings were written with LTL in mind, so there is no specific option to adapt them to LTLf. However any help toward this goal would welcome.

The easy part it to go through the list of all rewritings in https://spot.lrde.epita.fr/tl.pdf and find which ones do not work for LTLf, or possibly need to be adapted to use X[!] instead of (or in addition to) X.

The harder part is the introduce a new option in the rewriting code, locate all the rewriting rules that need to be updated, update the tl.pdf to match, add an option to ltlfilt to enable only these rules, and write test cases for all those changes.

Alternatively do you know of another software package that might do LTLf simplification?

I don't, but if you find some, I'm interested as well.