Currently our English to LTL translation is lacking. For instance, the
formula F(n → Gz), translates to “Eventually, globally, z holds is necessary for n holds”. We readily acknowledge that this recursively-generated phrasing is both confusing and unnatural.

I wonder if (given the small amount of randomness we already have in generating English) we could generate a few candidate English translations and then use a reasonable metric (maybe n-grams? smoothing?) to choose the best / most natural one?
I think relatively little work has been done in the world of LTL to English. Issues include :

• Compositionality gap: English is not fully compositional for temporal semantics
• English handles time through implicit quantifiers, whereas LTL requires explicit ones.
• Human language uses event schemas and narrative structure; LTL uses positions on a trace.
• English negation is structure-sensitive.