I have already stated on this board, twice, that this argument, when it is finally understood properly from a logical point of view, ends up in an argument about which type of modal logic you wish to employ (edit: I'm guessing it needs S5?).
And that is an argument that I don't think will lead to any useful result. There is really too much space for opinions in there.
The logic S5 in particular has one axiom that makes it unsuitable for many purposes. Namely, that "If X is possible, then X is necessarily possible". Intuitively this is appealing, but it breaks down if you are examining some system that evolves with time. It states that if something is possible now, then it will be always possible. For example, it is possible that I someday attend my granddaughter's wedding. However, for that to happen I must become a father of a child, something that has yet to happen. S5 would force us to conclude that even if I died without leaving children behind me, it would still be possible for me to attend that wedding.
This is the reason why logics that deal with time don't include that axiom, it would mess up the system to the point of unusability. Of course, there are also situations where S5 is appropriate and useful.
I do not pretend I understand how to choose which scheme of modal logic is legitimately appliable to this (or any other) argument.
The basic rule of the thumb is that you should be able to formulate your interesting property using the logic. Beyond that, it is largely "pick your own favourite". Though, it is useful if the logic in question has a proof system that can be effectively automated so that you don't have to compute all the conclusions by hand but can leave that to some black box. This is important when you get out of the domain of toy problems. (However, I have yet to encounter an example of a problem in philosophical logic that would be at the same time large enough to move out of the "toy problem" category and simple enough that we really could write it down completely.)
Like I said before, I have used mainly temporal logics and then in the context of model checking. This means that I have some system that is expressed as a labeled transition system and I want to check if some properties hold for that particular system. A transition system or a Kripke structure is basically just a collection of states linked together by a transition relation that tells what are the allowed state changes. In addition, each state has a set of propositions attached to it that are true in it. A labeled transition system adds a label for each transition so that we can keep track of our path through the states.
These labeled transition systems are very useful in modeling things. For a practical example, most communication protocols can be easily represented with them. Then we can use a temporal logic to express questions like "Is it possible that this system enters a deadlock?" or "If we suppose that the communication channel is not physically broken, do we finally get an answer for every request that we send?" and throw them to a solver that checks whether the formula is true in the structure and, if appropriate, either gives a path through the system for which the property holds or a path that is a counter example.