In practice we specify a system’s behavior as the conjunction of a safety and liveness property \(S \wedge L\). The safety-liveness decomposition is fundamental, as shown by Alpern and Schneider. Describing a system as a conjunction of arbitrary safety and liveness properties, however, can be dangerous.
Imagine we have a rectangular, two dimensional grid system, with an agent that starts at the bottom left of this rectangle i.e. at point \((0,0)\). The top right corner of the rectangle is a goal node that the agent is trying to reach.
We can impose an initial condition on the agent \((x=0, y=0)\) as well as a liveness requirement that says “eventually the agent reaches the goal”. Any path through our grid system that leads from the start point to the goal point satisfies our specification. We can think of a path in this example as a system behavior. We can then modify our system to add a region near the top of the grid that the agent is not allowed to enter (the shaded region in the illustration). With our specified liveness property, the agent should be able to take routes that avoid or go around the obstacle and reach the goal. If, however, we impose an additional safety property that the agent “can only move up or to the right”, then it’s possible for the agent to get stuck in a corner, without the ability to get out and ever reach the goal. In the illustration, the bottom path is one that satisfies our liveness property but not our safety property (since it winds left and right), the middle path satisfies both safety and liveness, and the path on the top left is one that gets stuck, unable to make any further progress. Indeed, any path that enters the gray shaded “dead ends” region is bound to get stuck in this way. That is, we can “paint ourselves into a corner” by simply taking steps that satisfy our safety property. More precisely, our system specification has allowed finite prefixes that satisfy the safety property but cannot be extended to satisfy our liveness property.
This motivates the concept of machine closure. It has also been referred to as feasibility. Lamport provides the following definition of machine closure: a pair of properties \((S, L)\) is machine closed if \(S\) is a safety property and every finite behavior satisfying \(S\) is a prefix of an infinite behavior satisfying \(S \wedge L\). Violation of machine closure means that there exists some safe finite prefix with no extensions that satisfy \(L\).
Note that machine closure depends on how we express a property \(P\) as the conjunction of a particular safety and liveness property. There may be a different safety liveness decomposition that permits the same behaviors as \(P\) but is machine closed. Based on the Alpern-Schneider decomposition theorem, any property \(P\) can be written as the conjunction of a safety property \(S\) and liveness property \(L\) such that \((S,L)\) is machine closed. The rectangular grid example given above also illustrates an intuitive aspect of non machine closed specifications, which is that satisfaction of both the safety and liveness property may require “foresight” (also referred to as “prescience”) on the part of the agent. That is, without knowledge of the entire layout upfront, by only making local moves the agent has no way of knowing that it may be traveling into a “dead end” region, that will prevent it from ever reaching its goal.
When we write specifications of real systems, nearly all of the time we want them to be machine closed. This is more or less intuitive if we think about a system as being defined or governed by a state machine, rather than by some pair of arbitrary temporal properties. When we specify a system as state machine, we naturally think about the allowed actions that can be taken at each step. Liveness constraints on a state machine should really be about fairness. They are like a thread scheduling policy, but don’t affect the possible actions that can be taken. In Fairness and Hyperfairness, Lamport defines a fairness requirement exactly as machine closure. That is, a property \(L\) is a fairness property for property \(S\) iff \((S,L)\) is machine closed.
The concept of machine closure is a reflection of the fact that arbitrary temporal (e.g liveness) properties are in some sense too expressive to be used as specifications for real systems. In general, specifications composed of arbitrary temporal properties may not correspond to “realizable” algorithms, since any real system (e.g. a program) has physical constraints on what it can do. For example, an algorithm cannot make decisions based on information from the future. When deciding on what step to take next, it can only take into account its current state. This is an inherent limitation of any system.
Note, however, that the expressivity of temporal properties can be useful in cases where we want to write a very abstract specification. We might not care whether a specification is directly realizable, since that is, in part, an essential aspect of a specification i.e. it should specify the what, not the how. If, broadly, we view specifications as either what specifications or how specifications, then in theory we want to write a what specification and show that a how specification implements it. And we want a how specification to be machine closed since it will presumably correspond, in some degree, to a real implementation. We don’t, however, need the what specification to be machine closed, if, for example, it’s simpler to write it in a way that is not machine closed. This is discussed in a thread here.
I also find it interesting to think about the concept of machine closure from the perspective of concurrent and distributed protocol design. Asynchronous, fault tolerant concurrent protocols require inherent trade offs between safety and liveness (e.g. FLP result, consensus numbers, etc.). So, if we are given some arbitrary safety and liveness property, it makes somewhat intuitive sense that it may not be “realizable” i.e. there may be cases where it’s impossible to maintain liveness while satisfying a given safety constraint. Perhaps machine closure and the techniques of safety-liveness decomposition provide one way to understand what liveness guarantees can be provided under given safety conditions, which would be relevant to some concurrent algorithms. This paper appears to explore this idea to some extent.