Hi Pascal, You might also want to have a look at chapter 8.1 of Specifying Systems ([1]), I found it helped me a lot in better understanding those temporal formulas. It also mentions the definition of "~>" in terms of "[]" and "<>". Regards, Valentin [1]: https://github.com/jackfoxy/SpecifyingSystemsWithContents/raw/master/Specifying%20Systems%2C%20TLA%2B.pdf