Variations on Safety
====================

Of special interest in formal verification are {\em safety\/}
properties, which assert that the system always stays within some
allowed region, in which nothing ``bad'' happens. Equivalently, a
property is a safety property if every violation of it occurs after a
finite execution of the system. Thus, a computation violates the
property if it has a ``bad prefix'', all whose extensions violate the
property.  The theoretical properties of safety properties as well as
their practical advantages with respect to general properties have
been widely studied.  The paper surveys several extensions and
variations of safety. We start with {\em bounded\/} and {\em
checkable\/} properties -- fragments of safety properties that enable
an even simpler reasoning. We proceed to a {\em reactive\/} setting,
where safety properties require the system to stay in a region of
states that is both allowed and from which the environment cannot
force it out.  Finally, we describe a probability-based approach for
defining different levels of safety.