Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification.
In this talk, I will present how we can achieve efficient composition of two-way transducers, mainly through the use of Reversible Transducers. Reversible machines are machine that are both deterministic and codeterministic.
I will show how any two-way transducers can be made reversible, while being easily composable. I will also show how these results can be extended to the setting of infinite words, which is the dedicated setting for model-checking for example.

TBA

Polyregular functions are the class of string-to-string functions definable by pebble transducers, an extension of finite-state automata with outputs and multiple two-way reading heads (pebbles) with a stack discipline. If a polyregular function can be computed with k pebbles, then its output length is bounded by a polynomial of degree k in the input length. But Bojańczyk has shown that the converse fails.
In this talk, I will sketch an easier proof of a stronger statement: for every k, there exists some polyregular function with quadratic growth whose output language differs from that of any k-fold composition of macro tree transducers, i.e. of any safe order-k tree transducer, and which therefore cannot be computed by a k-pebble transducer. Actually there is no need to know what these tree transducers are: the proof uses as a black box a powerful “bridge theorem” of Engelfriet and Maneth.
In fact, the proof of the bridge theorem implicitly uses a linearity argument, in the sense of linear logic. If time allows, I will briefly mention some ongoing work with Paweł Parys to extend this theorem to unsafe higher-order transducers, using a variant of the Taylor expansion of λ-terms and semi-quantitative coherence spaces.
Joint work with Sandra Kiefer and Cécilia Pradic: https://arxiv.org/abs/2301.09234

Adhesive categories are categories with structures that allows for some key results of graph rewriting theory to hold. There are also some weaker variations of this concept: rm-adhesive and rm-quasiadhesive categories.
I will present a formalization in Coq of the hierarchy of adhesive categories. This formalization relies on the Hierarchy Builder tool from the MathComp library. It is modular, with adhesive categories being at the top of a hierarchy which contains the weaker variants of adhesive categories and starts at the level of categories. Each level is equipped with several equivalent interfaces to define instances. It comes with a library of lemmas about more basic categorical concepts, such as pullbacks and regular monomorphisms.
This is my current work as a PhD student, supervised by Russ Harmer and Damien Pous.
The code can be found on this GitLab repository: https://gitlab.com/SamuelArsac/graph-rewriting

TBA

Comment reconnaître et connaître les plantes en 2024 ? Dans cet exposé nous nous interrogerons sur la manière dont l’informatique peut servir à construire des outils conviviaux – ou non – pour identifier les plantes. Nous présenterons l’exemple de Botascopia, un outil permettant de construire des clés de détermination adaptées à une flore locale et à destination du grand public. Nous détaillerons en particulier comment les descriptions morphologiques des plantes, issues des connaissances botaniques, peuvent être représentées et manipulées par un algorithme et un langage de programmation probabiliste dédié, permettant la construction d’un logiciel modulable et explicable.

On the one side, the formalism of Global Transformations comes with the claim of capturing any transformation of space that is local, synchronous and deterministic. The claim has been proven for different classes of models such as mesh refinements from computer graphics, Lindenmayer systems from morphogenesis modeling, and cellular automata from biological, physical and parallel computation modeling. The Global Transformation formalism achieves this by using category theory for its genericity, and more precisely the notion of Kan extension to determine the global behaviors based on the local ones. On the other side, Causal Graph Dynamics describe the transformation of port graphs in a synchronous and deterministic way.

In this work, we show the precise sense in which the claim of Global Transformations holds for them as well. This is done by showing different ways in which they can be expressed as Kan extensions, each of them highlighting different features of Causal Graph Dynamics. Along the way, this work uncovers the interesting class of Monotonic Causal Graph Dynamics and their universality among General Causal Graph Dynamics.

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.