A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis

TL;DR

This paper provides a general framework to encode system specifications and define corresponding certificates, and presents an automated approach to formally synthesise controllers and certificates, which contributes to the broad field of safe learning for control.

Abstract

An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verified by means of a function-based proof. However, the synthesis of controllers abiding by these complex requirements is in general a non-trivial task and may elude the most expert control engineers. This results in a need for automatic techniques that are able to design controllers and to analyse a wide range of elaborate specifications. In this paper, we provide a general framework to encode system specifications and define corresponding certificates, and we present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks to provide candidate control and certificate functions, whilst using SMT-solvers to offer a formal guarantee of correctness. We test our framework by developing a prototype software tool, and assess its efficacy at verification via control and certificate synthesis over a large and varied suite of benchmarks.

Figures (5)

• Figure 1: Pictorial depiction of relevant properties in this work. Here, $\mathcal{X}_I$ is the initial set, $\mathcal{X}_U$ the unsafe set ($\mathcal{X}_S$ is its safe complement), $\mathcal{X}_G$ the goal/target set, $\mathcal{X}_F$ the final set. (The entire state space is $\mathcal{X}$.) Here, a dashed background denotes that the corresponding set's existence is implied by the corresponding certificate, but that it is not explicitly defined in the property. Notably, this means that the set cannot be specified a-priori when defining the property: e.g., the invariant set $\mathcal{X}_G$ may be any size contained within $\mathcal{X}_F$. This motivates the construction of the additional certificates (and corresponding properties) ROA and RAR, which instead allow for a-priori set specifications.
• Figure 2: Euler Diagram depicting the semantic labels, arrive, avoid, and remain, associated with each certificate in this work. By the dashed line, we group properties that exhibit asymptotic stability. By the dotted line, we denote properties that exhibit (finite-time) reachability.
• Figure 3: Loss calculation block diagram. Blue indicates the inputs required for the loss calculation: namely the sampled data sets $D_\square$, the control and certificate network parameters $\theta_u$ and $\theta_c$, respectively. Red arrows represent the back-propagation steps, updating the networks' parameters during training. $f_u(x, \cdot)$ corresponds to the model in \ref{['eq:con-model']}, while $f(x)$ corresponds to the model in \ref{['eq:dyn-model']}.
• Figure 4: Enhanced CEGIS architecture within Fossil.
• Figure 5: Visualisations of a selection of certificates as either phase portraits (depicting the dynamics with relevant level sets of the certificate overlaid), or surface plots of the certificates (with relevant sets and level sets shown) from experiments in Table \ref{['tab:main']}. We show salient level sets as dashed lines, and denote others sets as follows. Dark blue: $\mathcal{X}_I$; Red: $\mathcal{X}_U$; light blue: $\mathcal{X}_S$; green: $\mathcal{X}_G$; orange: $\mathcal{X}_F$.

Theorems & Definitions (7)

• proof
• proof
• proof
• proof
• proof
• proof
• proof