Designing provably robust cyber-physical systems is an ambitious challenge, which usually requires employing multiple techniques from different branches of engineering and mathematics.
When the system under design is particularly complex, and there is uncertainty in the system or the environment, classical white-box methods from systems engineering are not feasible, and simulation-based approaches are the only viable option.
In this talk, I will present my work in optimization-based methods for system design that exploit Statistical Model Checking to provide formal guarantees on the robustness of the solution.
I will show different flavors of this approach in three application fields: the design of networks of anti-drone sensors in critical areas, the synthesis of robust controllers for complex industrial CPSs, and the model-based optimization of personalized therapies for cancer.

Joint work with Eugene Asarin, Cătălin Dima and Bernardo Jacobo Inclán.

Timed languages contain sequences of discrete events (“letters”) separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems.
The notion of bandwidth of a timed language characterizes the amount of information per time unit, encoded in words of the language observed with some precision $\varepsilon$.

In this talk, first we identify three classes of deterministic timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision $\varepsilon$: automata are either
– meager, with an $O(1)$ bandwidth,
– normal, with a $\Theta\left(\log\frac{1}{\varepsilon}\right)$ bandwidth,
– or obese, with $\Theta\left(\frac{1}{\varepsilon}\right)$ bandwidth.
We characterize the 3 classes thanks to 2 structural criteria, showing that the above asympotical classification is an actual partiion (there is no intermediate asymptotic class). The classification problem of a deterministic timed automaton is \PSPACE-complete.
Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri’s orbit graphs; the proofs are based on Simon’s factorization forest theorem.

Next, we propose a method, based on a finite-state simply-timed abstraction, to compute the actual value of the bandwidth of meager automata.
The states of this abstraction correspond to barycenters of the faces of the simplices in the region automaton.
Then the bandwidth is computed as $\log 1/|z_0|$ where $z_0$ is the smallest root (in modulus) of the characteristic polynomial of this finite-state abstraction.

Dans cet exposé, je vais présenter quelques résultats issus de mes travaux de thèse, dirigée par Julien Cervelle et Ludovic Patey, concernant le théorème de Ramsey en mathématiques à rebours. Je commencerai donc par une introduction à ce domaine, et présenterai quelques résultats de calculabilité qui nous seront utiles. J’en viendrai ensuite au théorème de Ramsey, sa relation aux mathématiques à rebours et les résultats qui le concernent. Enfin il sera question des résultats établis durant la thèse. Nous nous intéresserons tout d’abord à une variation du théorème de Ramsey pour les paires appelé SHER, qui est équivalent à plusieurs énoncés portant sur les arbres infinis. Puis nous verrons des résultats plus récents de séparation entre deux énoncés de Ramsey qui utilisent des techniques combinatoires dites de “cross-constraint”, ainsi qu’une variation de la notion d’hyperimmunité. Et, si le temps nous le permet, nous verrons un dernier résultat de séparation établi par forcing.