Imagine we have two LTL formulae: A and B. I would like to prove whether they are equivalent or not (the formulae can have the "Globally" operator, so the game is infinite).
To do so I have been reading about Ehrenfeucht-Fraïssé games, which I think fit well for this. So I plan to depict an arena for A and for B, and see whether the plays and strategies agree.
The problem is I do not have any example of this. For instance, how can I depict an arena of an LTL formula?
I find no information about this in the literature, apart from (maybe) this paper that I cannot access: https://dl.acm.org/doi/10.5555/2774283.2774790