  This paper presents a control synthesis algorithm for dynamical systems to
satisfy specifications given in a fragment of linear temporal logic. It is
based on an abstraction-refinement scheme with nonuniform partitions of the
state space. A novel encoding of the resulting transition system is proposed
that uses binary decision diagrams for efficiency. We discuss several factors
affecting scalability and present some benchmark results demonstrating the
effectiveness of the new encodings. These ideas are also being implemented on a
publicly available prototype tool, ARCS, that we briefly introduce in the
paper.
