GitLab

(GF(a)&GF(b)) | (GF(c)&GF(d)) is equivalent to (GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d)).

It's a bigger formula, but it can be translated into a one-state automaton.

Jan Strejcek:

ADL: we like to simplify GFa | GFb as GF(a|b) because GF(a|b) is easily translated as a deterministic automaton. In the same way, (GFa & GFb) | (GFc & GFd), which is currently translated as a non-deterministic automaton, could be rewritten as GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d) which will be translated as a deterministic automaton. Can this kind of rewriting be generalized?

I think I can provide a (partial) answer. The only non-obvious rule we have to add is the following:

for pure eventually formulae m1,m2 (roughly speaking, the formulae starting with F), the following equivalence holds: G m1 | G m2 <=> G (m1|m2)

With this rule and the standard rules

G f1 & G f2 <=> G (f1&f2)
distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
                or simply A | (C&D) <=> (A|C) & (A|D) applied twice
F f1 | F f2 <=> F (f1|f2)

one can transform (GFa & GFb) | (GFc & GFd) into G( F(a|c) & F(a|d) & F(b|c) & F(b|d)), which is enough to get determinstic automaton. A more interesting question may be "How to detect the situation when such rules should be applied". This especially applies to the distributivity as all other rules simply replace two modalities with one, which has usually positive effect on the translation and therefore the rules should be applied by default. I can imagine that distributivity will be applied only with --deter option and only to propagate disjunction downwards the syntactic tree (as disjunction is often a source of nondeterminism).

Jan:

ADL: It isn't as straightforward as it seems. For instance adding only the G(e1)|G(e2) = G(e1|e2) without distribution can be a serious regression:

G(Fa & Fb) | G(Fc & Fd): 3 states G((Fa & Fb) | (Fc & Fd)): 15 states G(F(a | c) & F(a | d) & F(b | c) & F(b | d)): 1 state

I think for this to work we have to guarantee that all pure eventualities will be rewritten as F(something).

I guess that you want to say that each pure eventuality formula can be rewritten into a conjunction of F(something) formulae. I'm afraid this doesn't hold. For example, GFa R Fb is a pure eventuality formula equivalent to GFa | GFb... Hmm, but there is no problem in this particular case. I have to think about it with a fresh mind.