Sooner Is Safer Than Later

It has been observed repeatedly that the standard safety-liveness classification for properties of reactive systems does not fit for real-time properties. This is because the implicit “liveliness” of time shifts the spectrum towards the safety side. While, for example, response—that “something good” will happen eventually—is a classical liveness property, bounded response—that “something good” will happen soon, within a certain amount of time—has many characteristics of safety. We account for this phenomenon formally by defining safety and liveness relative to a given condition, such as the progress of time.