Barrier functions (BFs) are Lyapunov-like functions which can be used to certify forward invariant of a set under a certain dynamica model. In words, they formally guarantee that the state of a system (e.g., position of robots, voltage values in a power plant) will remain inside a "safe set," forever [1]. For a given model and safe set, computing a BF is generally a difficult computational task which requires solving an infinite-dimensional optimization problem. To work arout this issue, several approximate, tractable procedures have been developed, from Sum-of-Squares programming to deep learning, all featuring different pro's and con's. One attractive sweet spot is represented by a method called counterexample-guided inductive synthesis (CEGIS), which alternates between solving a sample-based problem approximation (synthesis) and a check aided by formal verifiers (e.g., SMT with Z3 or dreal [2]). The flexibility of CEGIS allows a designer to use powerful tools to find a BF, such as neural networks. However, the verification task is generally a computational bottleneck.

In this thesis project, you will use CEGIS to compute a BF which tolerates faults, such as a broken sensor or actuator, while still certifying safe operation. This feature is crucial to help fault-tolerant control, for instance by switching to a robust controller before the system breaks down. The starting point of the thesis will be paper [3], where such a fault-tolerant BF is formalized. The supervisors has already started developing a CEGIS code framework to find a BF, which you will improve to speed up synthesis and verification. Related and/or different directions can be discussed with the supervisors.

This thesis project involves a - possibly remote - collaboration with TNO-ESI, Eindovhen [4].

[1] Abate A, Ahmed D, Edwards A, Giacobbe M, Peruffo A. FOSSIL: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. InProceedings of the 24th international conference on hybrid systems: computation and control 2021.

[2] Gao, Sicun, Soonho Kong, and Edmund M. Clarke. "dReal: An SMT solver for nonlinear theories over the reals." International conference on automated deduction, 2013.

[3] Ballotta, Luca, et al. "Fault detection via output-based barrier functions." European Journal of Control, 2025.

[4] https://esi.nl/