a formula to optimize
Here is a recurrence formula for which Spot (2.3.4) produces a non-deterministic automaton:
% ltl2tgba -D 'G(F(a & X(a)))'
Constructing the automaton by hand, it is natural to suggest the following deterministic automaton where each state remembers the last letter read:
Can we adapt the translation somehow to produce that?
I've checked a few translators, and most of them produce non-deterministic automata like Spot. The only exception I have found is ltl2da
from Owl, which produces the following deterministic automaton:
% owl-1.1.0/bin/ltl2da 'G(F(a & X(a)))'
This formula came in a discussion with @max about the translation of GF(a&Xa) & GF(a&!Xa)
which should also be translated to a 2-state automaton (but isn't, even by ltl2da
).