Environment-Friendly Safety

Of special interest in verification are safety properties, which
assert that the system always stays within some allowed region. For
closed systems, the theoretical properties of safety properties as
well as their practical advantages with respect to general properties
are well understood. For open (a.k.a. reactive) systems, whose
behavior depends on their on-going interaction with the environment,
the common practice is to use the definition and algorithms of safety
for closed systems, ignoring the distinction between input and output
signals. In a recent work, Ehlers and Finkbeiner introduced reactive
safety -- a definition of safety for the setting of open systems. 
Essentially, reactive 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. 

In this paper we continue their study and extend it to other families
of properties. In the setting of closed systems, each safety property
induces a set of finite bad prefixes -- ones after which the property
must be violated. The notion of bad prefixes enables a reduction of
reasoning about safety properties to reasoning about properties of
finite computations. We study reactive bad prefixes, their detection
in theory and in practice, and their approximation by either a
non-reactive safety property or by reasoning about the syntax of the
formula. We study the dual notion, of reactive co-safety properties,
and the corresponding theory of reactive good prefixes. For both
safety and co-safety properties, we relate the definitions in the
closed and open settings, and argue that our approach strictly extends
the range of properties for which we can apply algorithms that are
based on finite computations. Since the reactive setting is
particularly challenging for general properties, such an application
is significant in practice.