Abstraction-Refinement Based Optimal Control with Regular Objectives

TL;DR

This paper introduces an abstraction-refinement approach for synthesizing cost-efficient control strategies for discrete-time piecewise linear systems that satisfy linear-time temporal objectives.

Contribution

It develops a method to construct finite state weighted transition systems from partitions, providing suboptimal controllers with costs converging to the optimal.

Findings

Suboptimal controllers' costs converge to the optimal cost.

The method guarantees an upper bound on the original system's control cost.

The approach is demonstrated with examples using the OPTCAR tool.

Abstract

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.