What do formulas inside "[]" operate on?

[pascal.s...@xxxxxxxxx]

Hi, newbie here.

I was playing around with "~>" and wondering if it can be defined in terms of "[]" and "<>".

So I came up with this: I think "P ~> Q" is equivalent to "[](P => <>Q)". Unfortunately, I can't compare the two above Temporal Formulas with <=>, as TLC shouts "cannot handle" at me when I try..

When Lamport mentioned that applying a state formula to a behaviour is the same as applying it to the first state of that behaviour, similarly for action formulas, I came up with the intuition that "[]" and "<>" could therefore probably be seen as quantifiers over every possible suffix of a behaviour.

(I'm also assuming that what Lamport calls a behaviour is just a sequence of states. Please correct me if I'm wrong.)

This now leads me to believe that the above equivalence holds, because of the following argument:

Let P and Q be state formulas, and let B be a behaviour, then []P applied to B (as I understand it) means "(\A B_s \in suffixes(B) : P applied to B_s)". And since P applied to a behaviour is the same a P applied to the first state of that behaviour, then "[](P => <>Q)" means that for every state s in B where P is true, Q must hold true in some state t in the suffix of B, starting at s, which is equivalent to the definition of "~>".

Can anyone confirm or refute my assumptions, such as the assumption that everything inside of "[]" operates on a suffix? Thank you very much for your time and sorry for the long post.

Best regards
Pascal