  We consider abstraction-based design of output-feedback controllers for
dynamical systems with a finite set of inputs and outputs against
specifications in linear-time temporal logic. The usual procedure for
abstraction-based controller design (ABCD) first constructs a finite-state
abstraction of the underlying dynamical system, and second, uses reactive
synthesis techniques to compute an abstract state-feedback controller on the
abstraction. In this context, our contribution is two-fold: (I) we define a
suitable relation between the original system and its abstraction which
characterizes the soundness and completeness conditions for an abstract
state-feedback controller to be refined to a concrete output-feedback
controller for the original system, and (II) we provide an algorithm to compute
a sound finite-state abstraction fulfilling this relation.
  Our relation generalizes feedback-refinement relations from ABCD with
state-feedback. Our algorithm for constructing sound finite-state abstractions
is inspired by the simultaneous reachability and bisimulation minimization
algorithm of Lee and Yannakakis. We lift their idea to the computation of an
observation-equivalent system and show how sound abstractions can be obtained
by stopping this algorithm at any point. Additionally, our new algorithm
produces a realization of the topological closure of the input/output behavior
of the original system if it is finite-state realizable.
