Sooner Is Safer Than Later


Thomas A. Henzinger

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 "liveness" 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.

Information Processing Letters 43:135-141, 1992.


Download inofficial, sometimes updated PostScript / PDF document. © 1992 Elsevier.