Optimal Path Planning for ω-regular Objectives with Abstraction-Refinement

Abstract

This paper presents an abstraction-refinement based framework for optimal controller synthesis of discrete-time systems with respect to ω-regular objectives. It first abstracts the discrete-time “concrete” system into a finite weighted transition system using a finite partition of the state-space. Then, a two-player mean payoff parity game is solved on the product of the abstract system and the Büchi automaton corresponding to the ω-regular objective, to obtain an optimal “abstract” controller that satisfies the ω-regular objective. The abstract controller is guaranteed to be implementable in the concrete discrete-time system, with a sub-optimal cost. The abstraction is refined with finer partitions to reduce the suboptimality. In contrast to existing formal controller synthesis algorithms based on abstractions, this technique provides an upper bound on the trajectory cost when implementing the suboptimal controller. A robot surveillance scenario is presented to illustrate the feasibility of the approach.