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



You must log in to answer this question.