Hierarchical decomposition of LTL synthesis problem for nonlinear control systems

TL;DR

This paper introduces a hierarchical decomposition approach for synthesizing controllers for nonlinear control systems under LTL specifications, combining abstraction layers, discrete planning, and a new reachability over-approximation method.

Contribution

It presents a novel hierarchical framework for LTL control synthesis in nonlinear systems, integrating abstraction refinement and a monotonicity-based reachability method.

Findings

Successfully applied to a mobile robot motion planning problem.

Demonstrates effective handling of nonlinear dynamics and safety constraints.

Achieves systematic control synthesis through layered abstraction and planning.

Abstract

This paper deals with the control synthesis problem for a continuous nonlinear dynamical system under a Linear Temporal Logic (LTL) formula. The proposed solution is a top-down hierarchical decomposition of the control problem involving three abstraction layers of the problem, iteratively solved from the coarsest to the finest. The LTL planning is first solved on a small transition system only describing the regions of interest involved in the LTL formula. For each pair of consecutive regions of interest in the resulting accepting path satisfying the LTL formula, a discrete plan is then constructed in the partitioned workspace to connect these two regions while avoiding unsafe regions. Finally, an abstraction refinement approach is applied to synthesize a controller for the dynamical system to follow each discrete plan. The second main contribution, used in the third abstraction layer, is a new monotonicity-based method to over-approximate the finite-time reachable set of any continuously differentiable system. The proposed framework is demonstrated in simulation for a motion planning problem of a mobile robot modeled as a disturbed unicycle.