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 SAT-modulo-theory (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.

Model-based fault detection identifies anomalies by comparing a system's output with the prediction from a model. Although such a technique can be very powerful, it may suffer from the computational complexity of its underlying models, especially for large systems. An alternative approach that circumvents this cost increase uses barrier functions, which abstract the system's behaviour into a single value. In this paper, we propose a fault detection mechanism via output-based barrier functions, that does not require to estimate the full state, copes with noisy processes, and is tailored to safety-critical faults as given by a user-defined safe region. We leverage such a mechanism by introducing so-called p-fault tolerant sets, which guarantee that a faulty system requires at least p time steps before reaching any unsafe state. Our approach is validated through numerical experiments on two systems with linear and nonlinear dynamics, along with the classic three-tank model.

We employ the scenario optimisation theory to compute a traffic abstraction, with probability guarantees of correctness, of a PETC system with unknown dynamics from a finite number of samples. To this end, we extend the scenario optimisation approach to multiclass SVM in order to compute a map between the concrete state space and the intersample times of the PETC. This map allows the construction of a traffic abstraction, through an <inline-formula><tex-math notation="LaTeX">$\ell$</tex-math></inline-formula>-complete relation, that provides upper and lower bounds on the sampling performance of the concrete system. We further propose an alternative path to build such abstraction, first we identify the model and then apply a model-based procedure. Numerical benchmarks show the practical applicability of our methods for noiseless and noisy samples.

Closed-loop stability of control systems can be undermined by actuator faults. Redundant actuator sets and Fault-Tolerant Control (FTC) strategies can be exploited to enhance system resiliency to loss of actuator efficiency, complete failures or jamming. Passive FTC methods entail designing a fixed-gain control law that can preserve the stability of the closed-loop system when faults occur, by compromising on the performance of the faultless system. The use of Passive FTC methods is of particular interest in the case of underwater autonomous platforms, where the use of extensive sensoring to monitor the status of the actuator is limited by strict space and energy constraints. In this work, a machine learning-based method is formulated to systematically synthesise control laws for systems affected by actuator faults, encompassing partial and total loss of actuator efficiency and control surfaces jamming. Differently from other methods in this category, the closed-loop stability is formally certified. The learning architecture encompasses two Artificial Neural Networks, one representing the control law, and the other resembling a Control Lyapunov Function (CLF). Periodically, a Satisfiability Modulo Theory solver is employed to verify that the synthesised CLF formally satisfies the theoretical Lyapunov conditions associated to both the nominal and faulty dynamics. The method is applied to three marine test cases: first, an Autonomous Underwater Vehicle performing planar motion and subjected to full loss of actuator efficiency is investigated. Next, a study is conducted on a hybrid Underwater Glider with a pair of independent twin stern planes jamming at a fixed position. Finally, partial loss of effectiveness is considered. In all three scenarios, the system is able to synthesise stabilising control laws with performance degradation prescribed by the user. Unlike other machine-learning based techniques, this method offers formal stability certificates and relies on limited computational resources rendering it possible to be run on unassuming office laptops. An open-source software tool is developed and released at: https://github.com/grande-dev/pFT-ANLC.

The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-time stochastic processes in terms of richer discrete stochastic models, whose actions lead to nondeterministic transitions over the space of probability measures. The data-driven component of the proposed methodology lies in the fact that we only assume samples from an unknown probability distribution. We also rely on the model of the underlying dynamics to build our abstraction through backward reachability computations. The nondeterminism in the probability space is captured by a collection of Markov Processes, and we identify how this model can improve upon existing abstraction techniques in terms of satisfying temporal properties, such as safety or reach-avoid. The connection between the discrete and the underlying dynamics is made formal through the use of the scenario approach theory. Numerical experiments illustrate the advantages and main limitations of the proposed techniques with respect to existing approaches.

Performance and closed-loop stability of control systems can be jeopardised by actuator faults. Actuator redundancy in combination with appropriate control laws can increase the resiliency of a system to both loss of efficiency or jamming. Passive Fault-Tolerant Control (FTC) systems aim at designing a unique control law with guaranteed stability in both nominal and faulty scenarios. In this work, a novel machine learning-based method is devised to systematically synthesise control laws for systems affected by actuator faults, whilst formally certifying the closed-loop stability. The learning architecture trains two Artificial Neural Networks, one representing the control law, and the other resembling a Control Lyapunov Function (CLF). In parallel, a Satisfiability Modulo Theory solver is employed to certify that the obtained CLF formally guarantees the Lyapunov conditions. The method is showcased for two scenarios, one encompassing the stabilisation of an inverted pendulum with redundant actuators, whilst the other covers the control of an Autonomous Underwater Vehicle. The framework is shown capable of synthesising both linear and nonlinear control laws with minimal hyperparameter tuning and within limited computational resources.

Machine learning-based methodologies have recently been adapted to solve control problems. The Neural Lyapunov Control (NLC) method is one such example. This approach combines Artificial Neural Networks (ANNs) with Satisfiability Modulo Theories (SMT) solvers to synthesise stabilising control laws and to prove their formal correctness. The ANNs are trained over a dataset of state-space samples to generate candidate control and Lyapunov functions, while the SMT solvers are tasked with certifying the correctness of the Lyapunov function over a continuous domain or by returning a counterexample. Despite the approach's attractiveness, issues can occur due to subsequent calls of the SMT module at times returning similar counterexamples, which can turn out to be uninformative and may lead to dataset overfitting. Additionally, the control network weights are usually initialised with pre-computed gains from state-feedback controllers, e.g. Linear-Quadratic Regulators. To properly perform the initialisation requires user time and control expertise. In this work, we present an Augmented NLC method that mitigates these drawbacks, removes the need for the control initialisation and further improves counterexample generation. As a result, the proposed method allows the synthesis of nonlinear (as well as linear) control laws with the sole requirement being the knowledge of the system dynamics. The ANLC is tested over challenging benchmarks such as the Lorenz attractor and outperformed existing methods in terms of successful synthesis rate. The developed framework is released open-source at: https://github.com/grande-dev/Augmented-Neural-Lyapunov-Control.

We introduce a novel approach for the construction of symbolic abstractions - simpler, finite-state models - which mimic the behaviour of a system of interest, and are commonly utilized to verify complex logic specifications. Such abstractions require an exhaustive knowledge of the concrete model, which can be difficult to obtain in real-world applications. To overcome this, we propose to sample finite length trajectories of an unknown system and build an abstraction based on the concept of ℓ -completeness. To this end, we introduce the notion of probabilistic behavioural inclusion. We provide probably approximately correct (PAC) guarantees that such an abstraction, constructed from experimental symbolic trajectories of finite length, includes all behaviours of the concrete system, for both finite and infinite time horizon. Finally, our method is displayed with numerical examples.

We employ the scenario approach to compute probably approximately correct (PAC) bounds on the average inter-sample time (AIST) generated by an unknown PETC system, based on a finite number of samples. We extend the scenario optimisation to multiclass SVM algorithms in order to construct a PAC map between the concrete state-space and the inter-sample times. We then build a traffic model applying an l-complete relation and find, in the underlying graph, the cycles of minimum and maximum average weight: these provide lower and upper bounds on the AIST. Numerical benchmarks show the practical applicability of our method, which is compared against model-based state-of-the-art tools.

Formal abstractions of stochastic difference equations (SDEs) translate continuous-space processes into finite-state Markov models that can be automatically model checked against probabilistic specifications. These formal procedures carry an abstraction error that can be used to refine the outcomes of the model checking procedure from the abstract model to the concrete SDE. Parameter synthesis techniques aim at finding (any or all) model parameters that ensure the validity of a given specification, and are currently investigated by and large for finite-state parametric Markov models. In this work instead, we consider classes of parametric SDEs, and develop specific abstraction procedures relating the parameters in the obtained finite-state models to those of the concrete SDEs; we further show how parameter synthesis on the abstract models can be used to assert the satisfaction of given formal properties on the original parametric SDEs.