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. Motivation 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 rec...
