  Automata over infinite words, also known as omega-automata, play a key role
in the verification and synthesis of reactive systems. The spectrum of
omega-automata is defined by two characteristics: the acceptance condition
(e.g. B\"uchi or parity) and the determinism (e.g., deterministic or
nondeterministic) of an automaton. These characteristics play a crucial role in
applications of automata theory. For example, certain acceptance conditions can
be handled more efficiently than others by dedicated tools and algorithms.
Furthermore, some applications, such as synthesis and probabilistic model
checking, require that properties are represented as some type of deterministic
omega-automata. However, properties cannot always be represented by automata
with the desired acceptance condition and determinism. In this paper we study
the problem of approximating linear-time properties by automata in a given
class. Our approximation is based on preserving the language up to a
user-defined precision given in terms of the size of the finite lasso
representation of infinite executions that are preserved. We study the state
complexity of different types of approximating automata, and provide
constructions for the approximation within different automata classes, for
example, for approximating a given automaton by one with a simpler acceptance
condition.
