  This paper presents an abstraction-refinement method to synthesize control
inputs for a discrete-time piecewise linear system. The controlled system
behavior satisfies a finite-word linear-time temporal objective while incurring
minimal cost. An abstract finite state weighted transition system is
constructed from finite partitions of the state and input spaces by solving
optimization problems. A sequence of suboptimal controllers is obtained by
considering a sequence of uniformly refined partitions. The abstract system
satisfies the condition that the cost of the optimal control on the abstract
system provides an upper bound on the cost of the optimal control for the
original system. Furthermore, each suboptimal controller gives trajectories
that have the cost upper bounded by the cost of the optimal control on the
corresponding abstract system. In fact, the costs achieved by the sequence of
suboptimal controllers converge to the optimal cost for the piecewise linear
system. The tool OPTCAR implements the abstraction-refinement algorithm.
Examples illustrate the feasibility of this approach to synthesize
automatically suboptimal controllers with improving optimal costs.
