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

12 avril 2021

Milner et Alur entrent dans un bar

Daniele Varacca (LACL)

Alternating bisimulation for Alternating transition systems has been defined by Alur et al. It bears some ressemblence to the well known concept devised by Milner and Park for classical transition systems. The first aim of this work is to make the connection more formal: how can we make them look more similar to each other? Milner’s bisimulation is also a sound (and often complete) proof technique for contextual equivalences. What does “contextual equivalence” mean for alternanting transition systems, when there is no syntax, and therefore no notion of context? We propose an answer to this question, and we show that our version of alternating bisimulation is sound and complete for this generalised notion of contextual equivalence.
This is joint work with Romain Demangeon (LIP6) and Catalin Dima (LACL)

15 mars 2021

Left and Right Kan Extensions in Cellular Automata

Luidnel Maignan (LACL)

Paraphrasing the famous book of Saunders Mac Lane: “Everything is a Kan Extension”. However, depending on ones background of course, there might not be many examples that arise directly as Kan Extensions. In this talk, we show how the latter describes very naturally local to global definitions, as is the case for cellular automata for instance. Indeed the formal definition simply says “you have a local transformation and a way to compare arbitrary transformations? So simply choose the best global transformation possible!”.
This is based on my works with Antoine Spicher and Alexandre Fernandez on so-called “Global Transformations”

8 mars 2021

Computability, universality and quantum automata

Pablo Arrighi (LRI - University of Paris-Saclay )

I will draw a distinction between finite-dimensional quantum evolutions (“automata“) and infinite-dimensional evolutions (“operators”), and then explore their consequences upon two well-established concepts in Computer Science : computability and universality. Most of the results I will mention will rely on a decomposition of quantum operators, into quantum cellular automata—which is based upon the tacit assumption of a fixed partial order. Time-allowing, I will try to touch on the topical question of quantum partial orders.

22 février 2021

Threshold dot-depth one languages.

Nathan Grosshans (Theoretische Informatik / Komplexe Systeme, Universität Kassel)

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.

15 février 2021

A type theoretic approach to weak omega-categories


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.

15 février 2021

Proof Theory on Graphs

Matteo Acclavio (Université du Luxembourg)

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.

8 février 2021

Un cadre formel pour la conception correcte par construction de systèmes hybrides

Guillaume Dupont (INP Toulouse)

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.