Item

Abstract

This paper studies formal synthesis of controllers for continuous-space
systems with unknown dynamics to satisfy requirements expressed as linear
temporal logic formulas. Formal abstraction-based synthesis schemes rely on a
precise mathematical model of the system to build a finite abstract model,
which is then used to design a controller. The abstraction-based schemes are
not applicable when the dynamics of the system are unknown. We propose a
data-driven approach that computes the growth bound of the system using a
finite number of trajectories. The growth bound together with the sampled
trajectories are then used to construct the abstraction and synthesise a
controller.
Our approach casts the computation of the growth bound as a robust convex
optimisation program (RCP). Since the unknown dynamics appear in the
optimisation, we formulate a scenario convex program (SCP) corresponding to the
RCP using a finite number of sampled trajectories. We establish a sample
complexity result that gives a lower bound for the number of sampled
trajectories to guarantee the correctness of the growth bound computed from the
SCP with a given confidence. We also provide a sample complexity result for the
satisfaction of the specification on the system in closed loop with the
designed controller for a given confidence. Our results are founded on
estimating a bound on the Lipschitz constant of the system and provide
guarantees on satisfaction of both finite and infinite-horizon specifications.
We show that our data-driven approach can be readily used as a model-free
abstraction refinement scheme by modifying the formulation of the growth bound
and providing similar sample complexity results. The performance of our
approach is shown on three case studies.