For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. In this talk, I explain my recent works regarding these models and its timed version.

Temporal logics are a powerful tool to specify properties of computational systems.
HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages.
In recent work, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp’s theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp’s theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no auto-concurrency.
In previous work, we worked on lifting decidability and undecidability results from Timed Automata to a timed version of HDA, Higher Dimensional Timed Automata.

Cette présentation résume mes travaux de thèse autour de TLA+ et de son système de preuves. TLA+ est un langage de spécification basé sur la théorie des ensembles non typée. Son prouveur, TLAPS, génère et encode des obligations de preuve pour différents solveurs externes. Je me suis intéressée à l’encodage SMT dans l’optique de le rendre plus sûr d’utilisation, car il est apparu que l’ancienne version contenait des bugs. Je commencerai par exposer les bases de TLA+, puis je décrirai les étapes essentielles de l’encodage. L’innovation principale de ces travaux est le recours aux “triggers” de SMT, qui ont permis d’optimiser l’instanciation au premier ordre et de rendre l’encodage efficace en pratique.

Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In the work presented in this talk, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sens that we can exhibit such a controller.

Les assistants de preuves basés sur les types dépendants sont parmis les outils offrant les garanties les plus fortes sur la sécurité d’un logiciel. Cependant, pour des projets pratiques et de grande envergure, ils induisent un effort de preuve conséquent limitant leur adoption. Une situation communément rencontrée est l’utilisation de types de données efficaces, mais qui se prêtent peu au raisonnement, rendant les preuves très techniques. Une solution potentielle pour gérer cette complexité repose sur le principe d’univalence, proposé par Voevodski, qui postule que la bonne notion d’égalité entre les types est celles d’isomorphismes. Ce principe permet de transporter les algorithmes et leur preuves portant sur un type de données se prêtant au raisonnement mais inefficace pour le calcul vers un type de données efficace pour le calcul, mais moins simple pour le raisonnement. Malheureusement, le principe d’univalence est incompatible avec celui d’unicité des preuves d’identités (UIP), un autre principe permettant souvent de simplifier les raisonnements. Cela signifie qu’en pratique, travailler avec le principe d’univalence nécessite de gérer les preuves d’identités finement, ce qui est complexe. Dans cet exposé, je vais présenter mes travaux et une direction de recherche pour simplifier cette tache. Cette direction s’appuye sur un outil que je développe appelé CaTT, permettant de décrire la structure algébrique des types d’identités. Je montrerais comment le travail dans cet outil peut être partiellement automatisé, et présenterai un plug-in de Coq permettant de générer des calculs sur les termes d’identités. Cela permet de réduire l’effort de preuve à fournir pour gérer les types d’identités.

Je vais présenter deux méthodes de réduction pour les systèmes différentiels engendrés par des modèles Kappa, un langage de réécriture de graphes à sites.

La première étudie le flot d’information entre les différentes régions des espèces biomoléculaires.
Ceci permet d’identifier des corrélations qui n’ont pas d’influence sur la dynamique du système.
Les oublier engendre un changement de variable qui permet de réduire la dimension des équations différentielles.

La seconde est une méthode de troncation que l’on applique à un modèle de polymères.
Cette approche est conservative : elle est basée sur l’approximation de l’état du systèmes par des intervalles, dont les bornes évoluent selon des équations différentielles.

Dans les deux cas, les réductions sont prouvées correctes, grâce à des raisonnements symboliques sur les motifs de graphes à sites.
Ces raisonnements permettent des relations numériques entre les concentration de motifs et simplifier l’expression de la dérivée de leur concentration.

In this talk, I will present a game-theoretic approach to formalize fair exchange protocols under assumption of rational but possibly malicious agents. This framework is more expressive than previous frameworks for rational fairness.

In this joint work with Léonard Brice, Jean-François Raskin, Guillaume Scerri, and Marie Van Den Bogaard, we establish a strong link between our framework and concepts in game theory. More precisely, we show that the correctness conditions induced by our framework are strongly related to the concept of Strong Secure Equilibrium. This link with game theory allows us to develop efficient algorithms for the verification problems and we show that our algorithms have tractable complexity when the number of players is fixed, which is relevant in practice as the number of agents often remains small.

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.

Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. An important problem for conformance checking is to align a log trace with a model, that is, to find the minimal changes necessary to correct a new observation to conform to a process model.

The subject of this work is to study conformance checking for timed models, that is, process models that consider both the sequence of events in a process as well as the timestamps at which each event is recorded. We set our problem of timed alignment and solve two cases, each corresponding to a different metric over timed traces.

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