Skip to content

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)))'

ndet

Constructing the automaton by hand, it is natural to suggest the following deterministic automaton where each state remembers the last letter read:

det

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)))'

ltl2da output

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).

Edited by Alexandre Duret-Lutz