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

Understand

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.