Can we have reachability properties in TLA⁺?

We will go over two questions:

1. Is it possible to model-check reachability properties in TLA⁺ using TLC, the finite-state model checker? (Yes, definitely, but not without changing TLC)
2. Are reachability properties actually kosher by TLA⁺ semantics, or some kind of hideous intrusion of branching-time logic into the linear-time logic of TLA? (It’s fine, suprisingly!)

TLA⁺ already has reachability - kind of!

One of the more prominent (and weird2) operators in TLA⁺ is ENABLED. ENABLED A evaluates to true in a given state if action A can be taken in that state. The most common application of it is to check []ENABLED Next. This just says that it is always possible for your system to take another non-stuttering step. If this ever becomes false, your system is deadlocked! A very useful property, so much so that TLC checks it by default.3

ENABLED also lets you write the most basic reachability property, which is asking whether it is possible to reach a state in a single step. The property [](ENABLED Next /\ P') checks that you can always reach state P within a single step. TLC will check this today. However, it isn’t very useful. We usually want to know whether P can be reached in multiple steps. Lamport defines another operator, which he writes using the plus-superscript character ⁺.4 Its meaning will be familiar to anybody who knows regular expressions: it means one or more actions can be concatenated together. Lamport thus expresses full reachability properties as [](ENABLED [Next]_v^+ /\ P'), meaning one or more Next steps (or stuttering) can be taken to reach P instead of just one. This is quite an ugly formula written in ASCII; here it is all gussed up:

$ \Box\text{E}([Next]_v^+ \land P^{\prime}) $

TLC cannot currently check this property; it exists only as a figment in Lamport’s imagination. It also looks suspiciously like branching-time logic. Heresy! More on this later.

What TLC can and could check

Beyond ENABLED, TLC recently added support for basic reachability properties. These are still in beta, so you have to declare them in your model file as _POSSIBLE P. This does not check reachability from every system state; instead, it checks whether P can ever be satisfied at all, by any behavior starting in one of the initial states. You can read the motivation here, which is mostly about functioning as a “unit test” for your spec5. Checking _POSSIBLE is straightforward in TLC’s regular breadth-first search: if P is never hit by the time state exploration terminates, then report a failure. It was also recently figured out that _POSSIBLE offers a more ergonomic way of expressing trace validation, so it seems likely to stick around in the language.

What about full possibility/reachability properties? Can we check that P is reachable from every system state? TLC could certainly check those, but it would take more work. Thankfully this work has the shape of adding an additional isolated pass to model-checking instead of intertwining itself with existing machinery, so it could be viable to implement with limited risk of breaking things. The algorithm to use is called backward reachability. After the full state graph has been explored, write a pass that does breadth-first search on the state graph in reverse , starting from every state satisfying P and proceeding through every state that transitions to those states. If you have any unexplored states left over at the end, you know P isn’t reachable from those states so report a violation. Those leftover states even give a nice counterexample to start debugging!

Whether this will ever be implemented in TLC is unknown, but it seems like not a bad idea.

Sneaking in branching-time reasoning

Here I’ll do my best to explain the trick Lamport cooked up to get something that looks like branching-time reasoning into a linear-time logic. Just to forewarn, this section will be substantially more technical than the others. The semantics of TLA⁺ fundamentally define a specification as a set of infinite linear behaviors. This set of behaviors is itself generally infinite6. So within this infinite set of infinite linear behaviors, what could we possibly mean when we say REACHABLE P? Conventionally, TLA⁺ formulas have to apply to every behavior in this set. But we aren’t interested in whether every behavior actually reaches P; we want to know whether every behavior could have reached P! This kind of speculative future reasoning is entirely at home in branching-time logic but alien to linear-time logic.

The fundamental trick is to abuse fairness assumptions. A fairness assumption is a predicate you can use to filter the set of behaviors. For an example of common usage, a system that just sits there not doing anything (stuttering forever) is a perfectly valid behavior of a conventional TLA⁺ specification, but it isn’t very interesting. Thus many specs, if they want to check liveness properties like “eventually the system reaches a goal state”, will disallow those uninteresting behaviors with a fairness assumption like “if an action is continually enabled, it must eventually be taken”. Informally, I like to think of fairness assumptions as adding ocean currents to your specification that broadly nudge it toward desired states. Your system can still run around the entire state space, but it can’t get stuck somewhere forever without the current pushing it toward more productive behavior. Fairness assumptions are usually how you encode the “happy path” of your system like how sending a network message eventually succeeds, that kind of thing.

A fairness assumption is machine-closed if it does not keep the system from rejecting finite behaviors, only infinite ones - like rejecting the behavior that sits there stuttering and doing nothing forever7. More formally stated, every finite system behavior prefix must be extensible in a way that satisfies your fairness assumption, if your fairness assumption is machine-closed. In non-gibberish, this means that at any given moment in a behavior, it can wake up and be like “oh shoot, I forgot I need to satisfy the fairness assumption!” and then it can take a bunch of actions and go do that. The behavior can never reach a point after a finite series of steps where it’s beyond redemption. You may have noticed this “finite prefix must be extensible in a way that satisfies something” language looks a bit like talking about speculative future execution! And that’s the key to it all.

Suppose you want to check whether state \(P\) is reachable from every possible system state. If this were true, then some subset of system behaviors will include state \(P\). In fact, a subset will include \(P\) infinitely many times. In TLA⁺-ese, they satisfy the formula \(\Box \Diamond P\)8. What if you could then write a machine-closed fairness assumption \(F\) which admits only a very restrictive set of system traces, all of which satisfy \(\Box \Diamond P\)? Then, by the definition of machine closure, every finite prefix of the specification can be extended to satisfy \(\Box \Diamond P\)9. Thus every finite prefix admitted by the specification can reach \(P\)! Semantically valid reachability properties in TLA⁺! Written as:

$ (Spec \space \land \space F) \Rarr \Box \Diamond P $

So we have reduced the problem of stating “is \(P\) reachable by all states” to finding a suitable fairness assumption. Skeptical readers might rightfully believe I have stuffed quite a bit into that detail. Like sure if some magical fairness assumption drops out of the sky that is 1. machine-closed, and 2. somehow uniquely picks out traces satisfying \(\Box \Diamond P\) then I guess this works. But what reason do we have to believe that such a fairness assumption exists? And how could we actually derive it in reality for some arbitrary specification?

Constructing a fairness assumption

First we should give people an opportunity to bail out here. If all you care about is model-checking finite-state systems for reachability, we’ve shown that reachability probabilities work in linear-time logic! It isn’t some unmendable rupture in TLA⁺ semantics to talk about reachability. Go bother the TLA⁺ mailing list about adding reachability checking to TLC. The rest of this section will only appeal to the weirdos who want to formally prove things about infinite-state systems.

To reiterate, if you want to prove that a spec satisfies reachability property \(P\), it suffices to derive a machine-closed fairness assumption \(F\) such that:

$ (Spec \space \land \space F) \Rarr \Box \Diamond P $

There is a generalized existence construction for \(F\) given in Lamport’s Proving Possibility Properties, so if \(P\) actually is reachable then a suitable fairness assumption must exist, but there isn’t a way to derive \(F\) mechanically in a way that makes it easy to reason about in proofs; it requires creativity!

Let’s work on an example. Consider a spec of a single variable, \(x\), serving as a counter that can either increment or decrement:

$ Up ≜ x^{\prime} = x + 1 $ $ Down ≜ (x > 0) \land x^{\prime} = x - 1 $ $ Next ≜ Up \lor Down $ $ Spec ≜ (x = 1) \land \Box[Next]_x $

Suppose we want to prove that \(x = 0\) is always reachable, which of course it is. What fairness assumption \(F\) can we come up with which is both machine-closed and ensures \(\Box \Diamond (x = 0)\)?

Our first attempt might be to play it safe & familiar with \(F = SF_x(Down)\). Any fairness assumption composed of conjunctions of weak or strong fairness of sub-actions of \(Next\) will always be machine-closed. However, this is insufficient. The behavior that takes two \(Up\) steps for every one \(Down\) steps satisfies this \(F\), while never reaching \(x = 0\):

$ 1 \rightarrow 2 \rightarrow 3 \rightarrow 2 \rightarrow 3 \rightarrow 4 \rightarrow 3 \rightarrow 4 \rightarrow 5 \rightarrow \ldots $

It must be accepted that we have to abandon the usual safe ways of constructing machine-closed fairness assumptions and give trust to our own ability to prove that a potential formula is machine-closed. A good second attempt along this new line of attack is \(F = \Diamond \Box [Down]_x\): at a certain point the behavior says damn it all and only ever decrements. This is promising! If it only ever decrements, then it will head monotonically toward \(x = 0\)! It’s also machine-closed, since any behavior can stop at any point and just start decrementing. Unfortunately this fails because it allows perpetual stuttering:

$ 1 \rightarrow 1 \rightarrow 1 \rightarrow 1 \rightarrow 1 \rightarrow \ldots $

The fix is simple and familiar: conjoin it with weak fairness of \(Down\):

$ F = \Diamond \Box [Down]_x \land WF_x(Down) $

This is also machine-closed, and it certainly ensures \(\Box \Diamond (x = 0)\). So we’ve done it! We can use conventional liveness proof techniques10 to prove the reachability of \(x = 0\) from every state.

Actually our example is suggestive of a broader pattern. For defining \(F\) for an arbitrary spec, a decent starting point has the form:

$ F = \Diamond \Box [A]_v \land SF_v(A) $

Where \(A\) is an action (not necessarily an exact sub-action of \(Next\)) which would bring every state in the system closer to \(P\). So any behavior can at any point drop everything and head directly toward \(P\). The particulars will, of course, depend on your spec.

Applications to eventual consistency

In a previous post, I wrote a model of an eventually-consistent system (a conflict-free replicated datatype). Eventually-consistent systems have the property that each replica will always be slightly out of sync with the others, but if transactions stop flowing then all replicas are guaranteed to eventually converge to the same view of the system. I didn’t realize it at the time, but this is a reachability property! We want the system to always be able to converge, not that it necessarily always will! I ended up expressing this in a clumsy way by having an artificial boolean flag which could trigger at any time to stop new transactions, then checked that when the flag was true the system eventually converged. Now armed with the above knowledge of expressing reachability properties in TLA⁺, the flag could have been a fairness assumption instead! Something like this was actually suggested at the time, although I did not understand it then.

So actually TLC does support checking reachability properties now, as long as the user expresses them in the \((Spec \space \land \space F) \Rarr \Box \Diamond P\) formalism! Quite a tall order, since I with my decade-plus of TLA⁺ experience didn’t understand that method until writing this very blog post. Implementing reachability checking in TLC as its own thing with a backward reachability pass would be a tremendous improvement in usability.

Discussion

• lobste.rs
• Mastodon
• LinkedIn
• Hacker News
• TLA⁺ mailing list
• * *

1. Full disclosure, I accomplished this by asking GPT-6 Astra lots of questions about that section and digesting the answers. However, this blog post is entirely human-written using my own understanding that I’ve now developed as a result. Writing it is a way of explaining it back to myself as well as others. ↩︎
2. This deserves a post by itself, but read section 6.4.4.3: The Trouble with Enabled in A Science of Concurrent Programs for more info about how weird this operator is; it breaks logical substitution rules! ↩︎
3. You get TLC to skip deadlock checking by passing the -deadlock CLI flag. Yes this is a bad name. You try coming up with a better one! ↩︎
4. Just like in the stylized name of TLA⁺ itself! ↩︎
5. In ye olden times of a couple months ago, these unit tests were accomplished by intentionally writing an invariant you expected to fail, just to see TLC spit out a violation trace so you knew some part of your state space was actually reachable. ↩︎
6. You can make your behavior set have any finite cardinality \(N \in \natnums\) by transitioning to one of \(N\) initial states then stuttering forever, but any spec permitting an action to change a variable in its definition of \(Next\) must have an infinite number of behaviors. ↩︎
7. I think it’s more fun to call this property non-prescient instead of machine-closed. With a non-prescient/machine-closed fairness assumption, your system can evolve naturally without knowing that venturing into some part of the state space will keep it from reaching a goal state - and thus presciently avoid venturing into that part. So generally you want your fairness assumptions to be non-prescient/machine-closed, because computers do not yet function as spacing guild navigators and it would be nonsensical to specify them that way. William Schultz has a very nice post illustrating this prescience concept graphically. ↩︎
8. This is true even if \(P\) is an absorbing state like permanently turning off a computer, since a stuttering step in state \(P\) satisfies \(\Diamond P\) and \(\Box \Diamond P\). ↩︎
9. Why not just \(\Diamond P\)? Because then you could have a finite prefix which has already visited \(P\) and thus can be extended to satisfy your fairness assumption with literally any behavior, but the last state of the prefix might not be able to reach \(P\) again. We want to catch the possibility that after reaching \(P\) once, states reachable after \(P\) cannot themselves get back to \(P\). ↩︎
10. See section 4.2.4 of A Science of Concurrent Programs , titled Temporal Logic Reasoning , and subsequent sections. ↩︎

tlaplus