Dot-depth one languages are regular languages for which membership of words
basically depends on the sequences of factors they contain. This class of
languages does also correspond to the Boolean closure of the fragment of first
order logic with successor where only existential quantification is allowed.

I this talk, I will present a new class of regular languages that is a
restriction of the class of dot-depth one languages where factor-detection
only works up to a certain threshold. The main motivation behind its
definition is to capture the effect of intersecting the class of dot-depth one
languages with another well-known class of languages: the one of unambiguous
polynomials. I shall explain why considering such a new class is interesting,
give some properties of it and establish its links with other classes of
languages. I will finish with some research avenues suggested by my work on
threshold dot-depth one languages.

Weak omega-categories are a very challenging concept to study rigorously in mathematics, as the axioms defining them are very intricate and complicated to verify. In this talk I will present a way of dealing with this complexity algorithmically, by designing a language relying on dependent type theory. This language allows for the implementation of an interactive theorem prover “CaTT” dedicated to work with weak omega-category. I will then present the semantics of this language and formally relate its models with anterior notions of weak omega-categories, which is the main contribution of my PhD thesis.

video de l’exposé

Exceptionnellement deux séminaires aujourd’hui : celui-ci est à 15h15.

Logic and proof theory provide methods and tools used in areas such as formal verification and model checking. However, when we model processes-as-formulas, formulas are not expressive enough: they can model only some processes, those admitting a series-parallel decomposition, but they cannot handle the more general cases.
To overcome this limitation and develop new proof-theoretical tools for process analysis, in this talk I present a proof system based on unoriented graphs instead of formulas.

After showing how this system can find applications in process analysis, I will show some basic properties of the system.

Vidéo de l’exposé

Les systèmes hybrides sont des systèmes qui intègrent des comportements discrets (ordinateurs, calculateurs) et des comportements continus (phénomènes physiques à contrôler). Les systèmes hybrides sont variés et versatiles, et de ce fait occupent une place de plus en plus importante dans notre vie quotidienne, que ce soit dans le cadre d’objets connectés ou pour des applications critiques telles que des voitures autonomes ou des avions.

La nature hybride de ces systèmes les rend particulièrement difficiles à vérifier : les méthodes formelles classiques sont adaptées à leurs parties discrètes, et leurs parties continues est l’objet d’étude de la théorie du contrôle, mais intégrer ces deux aspects au même niveau dans le processus de conception et de vérification de ces systèmes est encore un défi majeur du domaine.

Dans le cadre de nos travaux, nous avons mis au point un cadre formel dont le but est la conception correcte par construction de systèmes hybrides. Ce cadre se base sur la méthode Event-B, dont il exploite le mécanisme d’extension ainsi que l’opération de raffinement, afin de mettre à disposition un ensemble de patrons de conception formels, qui peuvent être utilisés et réutilisés pour concevoir tout type de système hybride, de manière incrémentale. Ces patrons ont été formellement prouvés en utilisant les outils de preuve de Event-B. Ce cadre sert par ailleurs de support à une méthode générique de conception formelle de ces systèmes, que nous illustrons sur divers études de cas.

An automata network (AN for short) is a finite digraph where each node holds a state, chosen among a finite set,
that evolves in function of the states of its inbound neighbors.
Time is discrete and all nodes evolve synchronously and in parallel, similarly to what happens in an cellular automaton.
In other terms, the differences between a cellular automaton and an automata network is that the
“grid” is an arbitrary finite digraph, and that different nodes may have different update functions.
ANs have been used to model neural networks, dynamics of expression and inhibition of genes,
distributed algorithms, and more.

Although ANs look like a model of computation, they are not Turing-complete, for they lack unbounded memory.
Still, they are subject to some kind of “Rice theorems”, i.e., results along the lines of:
“any nontrivial property of the function computed by an automata network is computationally hard to test”.
In this talk, we will review several results that fit this pattern,
as well as pieces of proof that hopefully may be reused in other contexts.

Vidéo de l’exposé

We revisit the notion of local simulation of a Cellular Automaton (CA), which allows to transform a cellular automaton into a closely related one with different local encoding of information.

This notion is useful to explore the solution space of many CA problems, in particular we investigate two well studied one dimensional CA problems, namely the Firing Squad Synchronization Problem and the Sequence Generator problem.

1. For the Firing Squad Synchronization Problem we exhibit many solutions that are minimal both in time (2n-2 for n cells) and, up to current knowledge, also in states (6 states). This improves from the solution proposed by Mazoyer in 1987; and more recently the 718 new solutions generated by Clergue, Verel and Formenti in 2018 with a cluster of machines.
Using local simulations, we show how to generate millions of such 6-state solutions.

2. The Sequence Generator problem on the CA model has been studied since at least 1960 and numerous generation algorithms have been proposed for a variety of non-regular sequences such as {2^n | n = 1, 2, 3, …}, the primes, Fibonacci sequences etc.
Using the 6-state solution of Kamikawa and Umeo of read-time sequence generator for the cubes {n^3 | n = 1, 2, 3, …}, we handcrafted a 5-state reduction for this solution and then showed how to generate several million of solutions from this 5-state solution.
It is notable that in contrast to the current ubiquity of cloud computing, we used only a modest personal computer thanks to the nice algorithmic properties of local simulations.

video de l’exposé

On one hand, one often contrasts open dynamical systems with “ordinary/closed” dynamical systems, while knowing that, formally, open dynamical systems are a particular case of dynamical systems in many instances. On the other hand, a closed dynamical system is essentially a (collection of) function from a set X to itself. How to formalize “open” functions from a set X to another set Y ? This building block is necessary when designing a system as a composition of many modules. Also, how to formalize “open” functors from a category C to another category D. This building block is necessary when the dynamical system has some notion of “locality” and “space”. These questions arose in the study of so-called Global Transformations, dynamical systems where the space might be arbitrary and evolving concurrently and synchronously. In this talk, we begin by formalizing the matter as directly as possible with respect to the intuition. Then we connect the obtained construction to existing frameworks via three points of view. This might be seen as a (pedagogical ?) entry point to many categorical ideas starting from the simple ground of cellular automata. This is based on works in progress with Alexandre Fernandez and Antoine Spicher.

Iterative conditional branching are used in sensitive environments, like the modular exponentiation in the RSA cryptographic protocol, but these algorithms are usually vulnerable against side-channel attacks and fault-injection attacks.
The Montgomery ladder algorithm for the modular exponentiation uses interleaved variables to protect the execution from these attacks.
We abstracted away the properties verified by the Montgomery ladder at every step of the computation, and formalized the conditions for more secure algorithms by using systems of equations.
We obtained the conditions for semi-interleaved (like the Montgomery ladder) or even fully-interleaved ladder algorithms, and proposed a fault-injection attack able to obtain bits of the secret against semi-interleaved ladders (including the original Montgomery ladder) but not against fully-interleaved ladders.
We also applied these equations to extend the Montgomery ladder for both the semi- and fully-interleaved cases, thus proposing novel and more secure algorithms to compute the modular exponentiation.
Thus, we captured a classe of secure algorithms, and proposed a general and fruitful methodology to detect or construct these algorithms for the targetted functions.

Successor-invariant first-order logic is the extension of first-order logic where one has access to an additional successor relation on the elements of the structure, as long as the validity of formulas is independent on the choice of a particular successor.

It has been shown by Rossman that this formalism allows to express properties that are not FO-definable.
However, his separating example involves dense classes of structures, and the expressive power of successor-invariant first-order logic is an open question for sparse classes of structures.

We prove that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.