Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

7 décembre 2020

Successor-Invariant First-Order Logic on Classes of Bounded Degree

Julien Grange (INRIA Rennes)

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.

30 novembre 2020

Falsification of Cyber-Physical Systems with Constrained Signal Spaces

Benoît Barbot (LACL)

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.

23 novembre 2020

Implémentations matérielles efficaces des modèles de calcul non-conventionnel

Serghei Verlan (LACL)

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.