On the Construction of Fine Automata for Safety Properties

Of special interest in formal verification are safety properties,
which assert that the system always stays within some allowed region.
Each safety property \psi can be associated with a set of bad
prefixes: a set of finite computations such that an infinite
computation violates \psi iff it has a prefix in the set.  By
translating a safety property to an automaton for its set of bad
prefixes, verification can be reduced to reasoning about finite words:
a system is correct if none of its computations has a bad prefix.
Checking the latter circumvents the need to reason about cycles and
simplifies significantly methods like symbolic fixed-point based
verification, bounded model checking, and more.

A drawback of the translation lies in the size of the automata: while
the translation of a safety LTL formula \psi to a nondeterministic
Buchi automaton is exponential, its translation to a tight bad-prefix
automaton --- one that accepts all the bad prefixes of \psi, is doubly
exponential. Kupferman and Vardi showed that for the purpose of
verification, one can replace the tight automaton by a fine automaton
--- one that accepts at least one bad prefix of each infinite
computation that violates \psi. They also showed that for many safety
LTL formulas, a fine automaton has the same structure as the Buchi
automaton for the formula.  The problem of constructing fine automata
for general safety LTL formulas was left open. In this paper we solve
this problem and show that while a fine automaton cannot, in general,
have the same structure as the Buchi automaton for the formula, the
size of a fine automaton is still only exponential in the length of
the formula.