Hi Vincenzo,
(Sorry for the delay, I just found your email in the middle of hundreds of spams that were waiting to be moderated...)
Vincenzo Tramo vv.tramo@gmail.com writes:
When attempting to translate an LTL formula into a Büchi automaton with the following inputs, the function does not terminate:
INPUT 1 alive & sing & (alive U G!alive) & G(!alive | last | (sing <-> X (alive & !sing))) & F(alive & last & sing) & (p0 R (!alive | (p0 & ! sing) | ((p1 R (!alive | p3 | (p1 & !sing))) & F(alive & p1 & p3)))) & (p4 U (alive & p5 & (p4 | sing))) & (Xp0 U (alive & (p3 R (!alive | (p3 & !sing) | (p4 U (alive & (p4 | sing) & (p2 | (p2 U (alive & (p2 | sing) & (p3 R (!alive | p10 | (p3 & !sing)))))))) | G(!alive | p4))) & (sing | Xp0)))
The above looks like an LTL formula generated from LTLf, so a deterministic BA will always exist for that. Building this DBA is reasonably fast:
% ltl2tgba -D -F input1.ltl --stats="%s st., %e ed., %r sec." 381 st., 7269 ed., 0.67422 sec.
If I drop option -D, it becomes slow because Spot will try to simplify the non-deterministic Büchi automaton using simulation-based reductions. I've found that if we activate only direct-simulation, the translation is efficient:
% ltl2tgba -x simul=1 -F input1.ltl --stats="%s st., %e ed., %r sec." 395 st., 6290 ed., 0.601192 sec.
However, the reverse simulation is very slow: with ~390 equivalence classes and some state having a up to 250 incoming edges, building the BDD signature of some of these states is very expensive, and BuDDy spends a lot of time running its garbage collector and allocating more memory. At this point, it's not clear to me how we could improve that.
Switching to the matrix-based implementation of simulation-based reduction was successful too, but the size reduction is inferior:
% ltl2tgba -x simul-method=2 -F input1.ltl --stats="%s st., %e ed., %r sec." 420 st., 6356 ed., 1.2033 sec.
I've created an issue to track any progress on that https://gitlab.lre.epita.fr/spot/spot/-/issues/599
INPUT 2
That second formula has 80 atomic propositions and looks highly random to me. Since we are dealing with algorithms that have 2^AP worst cases, do we have any to reason to believe it show be translated efficiently?
Alexandre