 Again, there is no right answer to this question. It all depends on what the fundamental characteristics are that one is trying to model. To express Nash equilibria in a coordination game, there is no need for a temporal logic-based formalism. On the contrary, if one wants to express backwards induction, then a language that does not make the sequential structure of the decision problem explicit is probably not the right one.