Continuous and discrete abstractions for planning, applied to ship docking

TL;DR

This paper introduces a hierarchical control framework combining continuous and discrete abstractions with formal methods and SOS programming to synthesize correct-by-construction controllers for complex nonlinear systems, demonstrated on ship docking.

Contribution

It presents a novel SOS-based continuous abstraction that explicitly accounts for control input-dependent errors, enabling efficient hierarchical control synthesis for high-dimensional systems.

Findings

Effective control synthesis for ship docking demonstrated

Lower error bounds achieved through input-dependent abstraction

Framework scalable to high-dimensional nonlinear systems

Abstract

We propose a hierarchical control framework for the synthesis of correct-by-construction controllers for nonlinear control-affine systems with respect to reach-avoid-stay specifications. We first create a low-dimensional continuous abstraction of the system and use Sum-of-Squares (SOS) programming to obtain a low-level controller ensuring a bounded error between the two models. We then create a discrete abstraction of the continuous abstraction and use formal methods to synthesize a controller satisfying the specifications shrunk by the obtained error bound. Combining both controllers finally solves the main control problem on the initial system. This two-step framework allows the discrete abstraction methods to deal with higher-dimensional systems which may be computationally expensive without the prior continuous abstraction. The main novelty of the proposed SOS continuous abstraction is that it allows the error between abstract and concrete models to explicitly depend on the control input of the abstract model, which offers more freedom in the choice of the continuous abstraction model and provides lower error bounds than when only the states of both models are considered. This approach is illustrated on the docking problem of a marine vessel.