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.

翻译：一个新兴的控制理论分支专门研究证书学习，其关注的是为自主或控制模型指定所需（可能复杂）的系统行为，随后通过基于函数的证明对其进行解析验证。然而，综合出符合这些复杂要求的控制器通常是一项非平凡任务，甚至可能令最专业的控制工程师感到棘手。这便催生了对自动技术的需求，使其能够设计控制器并分析大量复杂的规格说明。本文提出一个通用框架来编码系统规格说明并定义相应的证书，同时展示了一种自动化的控制器与证书形式化综合方法。我们的方法为控制领域的安全学习这一广阔领域做出贡献，利用神经网络的灵活性提供候选控制与证书函数，同时使用SMT求解器提供正确性的形式化保证。我们通过开发原型软件工具对框架进行测试，并在大量多样化的基准测试集上评估其在控制与证书综合验证中的有效性。