An iterative algorithmic implementation of input-output finite state approximations

The problem of finding finite state models of systems with quantized inputs and outputs has received much deserved attention. In particular, a notion of ρ/μ approximation was proposed and shown to be relevant to the problem of control synthesis. In this paper, we revisit a recently developed constructive algorithm for generating ρ/μ approximations for a class of systems, and we propose and analyze several algorithms for improving the computational efficiency and memory requirements of the construction. We demonstrate the use of this approach for synthesizing certified-by-design controllers for a simple illustrative example with reachability type specifications.