4 Jan
2021
4 Jan
'21
9:59 a.m.
Hi Homer!
"Walke, Homer" <homer_walke(a)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.
--
Alexandre Duret-Lutz