[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
What do formulas inside "" operate on?
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.