Properties that always hold, ie: invariants, should not have to be indicated by special notations. They should be unadorned. Special notations should only be used to indicate when a property does not always hold.
Lamport's Temporal Logic of Actions violates this principle in that a predicate P holds only in the initial state, and if you want to indicate that it always holds the you have to put a box symbol in front of it:
Similarly, in Daniel Jackson's Micromodularity Mechanism you have to use the keyword 'fact' to indicate that a predicate is invariant.
It seems obvious and natural to me that if a predicate P does not always hold then this should be indicated by an implication Q->P where Q is the condition under which P does hold.