Model Checking of Safety Properties
===================================

Of special interest in formal verification are
safety properties, which assert that the system always stays
within some allowed region.
A computation that violates a general linear property reaches a bad
cycle, which witnesses the violation of the property. Accordingly, 
current methods and tools for model checking of linear properties are
based on a search for bad cycles. A symbolic implementation of such a
search involves the calculation of a nested fixed-point expression over
the system's state space, and is often very difficult.
Every computation that violates a safety property has a finite prefix
along which the property is violated. We use this fact in order to
base model checking of safety properties on a search for finite bad
prefixes. Such a search can be performed using a simple forward or
backward symbolic reachability check. 
A naive methodology that is based on such a search involves a
construction of an automaton (or a tableau) that is doubly exponential
in the property. We present an analysis of safety properties that
enables us to prevent the doubly-exponential blow up and to use the
same automaton used for model checking of general properties,
replacing the search for bad cycles by a search for bad prefixes.