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.

Falsification has garnered much interest recently as a way to validate complex Cyber-Physical Systems (CPS) designs with respect to a specification expressed via temporal logics. Using their quantitative semantics, the falsification problem can be formulated as a robustness minimization problem. To make this infinite-dimensional problem tractable, a common approach is to restrict to classes of signals that can be defined using a finite number of parameters, such as piecewise-constant or piecewise-linear signals with fixed time intervals.

A drawback of this approach is that when the input signals must satisfy non-trivial temporal constraints, encoding these constraints into bounded domains for parameters can be difficult. In this work, to better capture temporal constraints on the input signal space, we use timed automata (TA) and make use of a transformation that allows sampling TA traces by sampling points in the unit box.

We exploit this transformation to efficiently encode constrained CPS signals in the robustness minimization problem. This transformation also allows us to define an effective coverage measure for the constrained signal space so as to provide quantitative guarantees when no falsifying behaviour is found. Additionally, the coverage measure is used to improve the black-box optimisation performance by detecting situations where the search is stuck near a local optimum. The approach is demonstrated on a modulator and a model of a car automatic transmission subject to constraints that describe usual driving patterns.

Les modèles de calcul non-conventionnel permettent d’avoir une approche différente pour la résolution des nombreux problèmes, plus particulièrement des problèmes d’optimisation et d’algorithmique parallèle. Dans la plupart des cas, les modèles sous-jacents sont massivement parallèles et ne peuvent pas être implémentés efficacement en logiciel sur des architectures courantes.

Nous nous sommes intéressés récemment par le développement des architectures matérielles spécialisées (en circuits logiques matériels à l’aide des FPGA) ce que permettrait d’avoir une exécution réellement parallèle des modèles correspondants. Afin d’obtenir des implémentations efficaces nous avons analysé les opérations possibles en FPGA et nous avons proposé des restrictions théoriques sur les modèles considérés ce que nous a permis d’obtenir des implémentations très efficaces (speed-up de l’ordre 10^5 par rapport aux réalisations logicielles et une vitesse de calcul à 10^8 étapes/s).

Ce qui est particulier dans notre démarche, c’est l’utilisation des résultats théoriques de la théorie des langages formels afin d’obtenir les résultats d’accélération cités ci-dessus. Nous allons montrer des exemples (concernant l’implémentation des différentes versions des systèmes à membranes) où l’efficacité de l’implémentation est une conséquence de la réduction du problème de simulation au problème du nombre des mots dans un langage rationnel. Nous allons également donner l’exemple de l’implémentation efficace des systèmes à membranes numériques où le point clef est la possibilité d’expression du problème en arithmétique de Presburger. Nous avons également montré que dans ce cas le modèle correspond à un système d’équations non-linéaires en différences finies et nous avons appliqué cette correspondance pour la création des contrôleurs matériels (extrêmement rapides – environs 10ns de temps de réponse) pour le problème du déplacement des robots à roues.

Nous allons également discuter des liens entre nos résultats et les langages par flots de données synchrones, plus particulièrement LUSTRE, ainsi que des questions liées à la vérification des modèles obtenus.

Vidéo de l’exposé

En ingénierie des exigences (IE) pour les systèmes critiques, au moins deux types de modèles sont nécessaires.

D’une part les exigences doivent être exprimées dans un langage qui puisse être compris par les différentes parties-prenantes qui participent à la construction du modèle d’exigences dans un but de validation. Dans la plupart des méthodes d’IE ce langage est graphique.

D’autre part, il faut un langage formel pour vérifier les exigences critiques. Le projet ANR FORMOSE avait pour objectif de construire une méthode formelle d’IE orientée modèles pour des systèmes critiques.

Nous avons développé une méthode d’IE orientée buts, SysML/KAOS, qui permet de décrire graphiquement les exigences à différents niveaux d’abstraction. Ce modèle des exigences est complété par un modèle de domaine pour décrire les entités du système et leurs propriétés. A partir de ces deux modèles, une spécification formelle Event-B est alors dérivée. Pour maintenir la cohérence entre les deux modèles graphique et formel, nous avons utilisé une technique de fédération de modèles qui consiste à définir un méta-modèle pour chacun des langages puis un modèle d’alignement qui permet de spécifier des liens dynamiques entre les deux méta-modèles. L’approche a été implémentée sur l’outil Openflexo.

Vidéo de l’exposé

Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers cause a triple exponential blow-up in the size of the inputs.
In this talk, I will present the class of reversible transducers, which are machines that are both deterministic and co-deterministic. This class enjoys polynomial composition complexity, even in the two-way case.

Although this class is not very expressive in the one-way scenario, I will show that any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, the composition of two-way transducers can be done with a single exponential blow-up in the number of states, enhancing the known algorithm from the 60s.

video de l’exposé