Compositional abstraction refinement for control synthesis

TL;DR

This paper introduces a compositional, specification-guided abstraction refinement method for control synthesis of nonlinear systems, enabling efficient controller design through subsystem decomposition and iterative partition refinement.

Contribution

It proposes a novel compositional approach that combines subsystem decomposition, assume-guarantee reasoning, and iterative abstraction refinement for control synthesis.

Findings

The method effectively enforces specifications on nonlinear systems.

It outperforms existing abstraction techniques in efficiency.

Numerical examples demonstrate successful control synthesis.

Abstract

This paper presents a compositional approach to specification-guided abstraction refinement for control synthesis of a nonlinear system associated with a method to over-approximate its reachable sets. Given an initial coarse partition of the state space, the control specification is given as a sequence of the cells of this partition to visit at each sampling time. The dynamics are decomposed into subsystems where some states and inputs are not observed, some states are observed but not controlled and where assume-guarantee obligations are used on the uncontrolled states of each subsystem. A finite abstraction is created for each subsystem through a refinement procedure starting from a coarse partition of the state space, then proceeding backwards on the specification sequence to iteratively split the elements of the partition whose coarseness prevents the satisfaction of the specification. Each refined abstraction is associated with a controller and it is proved that combining these local controllers can enforce the specification on the original system. The efficiency of the proposed approach compared to other abstraction methods is illustrated in a numerical example.