On Clopen Specifications
========================
{\em Bounded model checking} methodologies check the correctness of a
system with respect to a given specification by examining computations
of a bounded length. Results from set-theoretic topology imply that
sets in $\Sigma^\omega$ that are both open and closed ({\em clopen
sets\/}) are precisely bounded sets: membership of a word in a clopen
set can be determined by examining a bounded prefix of it. Clopen
sets correspond to specifications that are both safety and co-safety.
In this paper we study bounded specifications from this perspective.
We consider both the linear and the branching frameworks. In the
linear framework, we show that when clopen specifications are given by
word automata or temporal logic formulas, we can identify a bound and
translate the specification to bounded formalisms such as cycle-free
automata and bounded LTL. In the branching framework, we show that
while clopen sets of trees with infinite branching degrees may not be
bounded, we can extend the results from the linear framework to clopen
specifications given by tree automata or temporal logic formulas, even
for trees with infinite branching degrees. There, we can identify a
bound and translate clopen specifications to cycle-free automata and
modal logic. Finally, we show how our results imply that the bottom
levels of the $\mu$-calculus hierarchy coalesce.