upvote
You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.

A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.

Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.

reply
On top of what Andrew said, "failure as reachability" is a property of the implementing model checker, not the formalism itself! If you convert "we can win the game" to "it's not true that always we haven't won" and write that up as a TLA+ formula, you get `![](!won)". But that means "we win in every behavior", aka `<>won`!

A really good paper on the difference between "possible" and "eventual" is '"Sometime" is sometimes "not never"': https://dl.acm.org/doi/10.1145/567446.567463

reply