Joint work with Francesco Belardinelli, Vadim Malvone and Ferucio Tiplea

### May 17, 2021

*A Hennessy-Milner Theorem for ATL with Imperfect Information*

**Catalin Dima**

Skip to content
# Seminars 2020-21

Contact : seminar@lacl.fr
# On monday, at 2pm - UPEC CMC - Room P2-131

### May 17, 2021

*A Hennessy-Milner Theorem for ATL with Imperfect Information*

**Catalin Dima**
(LACL)

### May 10, 2021

*Size-varying reversible causal graph dynamics*

**Amélia Durbec**
(LIS, Aix Marseille University)

### April 12, 2021

*Milner et Alur entrent dans un bar*

**Daniele Varacca**
(LACL)

### March 29, 2021

*Rewriting Theory for Biochemical Reaction Systems*

**Nicolas Behr **
(Université de Paris, CNRS, IRIF)

### March 22, 2021

*À propos des réseaux d’automates booléens*

**Sylvain Sené**
(LIS, Aix Marseille University)

### March 15, 2021

*Left and Right Kan Extensions in Cellular Automata*

**Luidnel Maignan**
(LACL)

### March 8, 2021

*Computability, universality and quantum automata*

**Pablo Arrighi**
(LRI - University of Paris-Saclay )

### March 1, 2021

*Rational Players in Committee-based Blockchains*

**Yackolley Amoussou Guenou**
(CEA)

### February 22, 2021

*Threshold dot-depth one languages.*

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

### February 15, 2021

*A type theoretic approach to weak omega-categories*

**Thibaut BENJAMIN**
(CEA LIST)

We show that a history-based variant of alternating bisimulation under imperfect information is related to a variant of ATL with imperfect information by a Hennessy-Milner theorem. The variant of ATL we consider has a “common knowledge” semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition. The proof utilizes a bisimulation game between two coalitions, each composed of two agents, for which we provide a Gale-Stewart determinacy theorem. We notice that other semantic variants of ATL with imperfect information do not accomodate a reverse Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

Joint work with Francesco Belardinelli, Vadim Malvone and Ferucio Tiplea

Consider a network that evolves reversibly, according to

nearest neighbours interactions. Can its dynamics create/destroy nodes?

On the one hand, since the nodes are the principal carriers of information,

it seems that they cannot be destroyed without jeopardising bijectivity.

On the other hand, there are plenty of global functions from graphs to

graphs that are non-vertex-preserving and bijective. The question has

been answered negatively—in three different ways. Yet, in this paper we

do obtain reversible local node creation/destruction—in three relaxed

settings, whose equivalence we prove for robustness. We motivate our

work both by theoretical computer science considerations (reversible

computing, cellular automata extensions) and theoretical physics concerns

(basic formalisms towards discrete quantum gravity).

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)

The biochemistry platform Kappa (https://kappalanguage.org) offers high-performance simulation and static analysis algorithms for complex and real-life scale biochemical reaction systems. At the core of the system, a form of *rewriting theory* (of so-called site graphs) provides the semantics based upon which the notion of biochemical reactions is implemented.

In this talk, I will present recent original developments that investigate further the mathematical properties of the Kappa rewriting language. I will demonstrate that Kappa constitutes a typical example of a so-called restricted rewriting theory. Objects from some ambient category of graph-like structures are subjected to certain structural constraints to identify patterns (i.e., observable sub-structures) and fully specified biomolecules.

One of the core advantages of this new approach to rewriting theory in the life sciences consists of the compositional associativity properties carried by such restricted rewriting theories, which permits extending the static analysis toolkit to cover a class of pattern-counting observable moment evolution equations. Concretely, while state-spaces for realistic biochemical systems are typically prohibitively complex, it is envisioned that the study of the evolution of pattern-counts (i.e., roughly of functional groups) might prove a fruitful avenue to gain insights into the high-level behaviors of such systems.

Finally, time permitting, I will briefly sketch the latest stage of this development, namely the first-of-its-kind fully specified rewriting semantics for organo-chemical reaction systems.

The talk is based upon joint work with J. Krivine (IRIF), J.L. Andersen and D. Merkle (U Odense).

Les réseaux d’automates booléens constituent un modèle mathématique dans lequel des entités (les automates) à états booléens interagissent les unes avec les autres au cours du temps (discret). C’est un modèle qui est apparu au moment où l’informatique moderne est née. Il a été introduit sous une forme spécifique dans les années 1940 par McCulloch et Pitts avec leur travail sur les réseaux de neurones formels. Il a par la suite été largement développé en suivant plusieurs lignes d’intérêt, avec entre autres les modèles de calcul, les systèmes dynamiques et la modélisation des réseaux biologiques.

Dans ce séminaire, nous évoquerons les réseaux d’automates booléens sous un angle plutôt théorique, en laissant de côté les liens qu’ils entretiennent avec la biologie. Plus précisément, nous parlerons de certaines des lois générales historiques connues à leur sujet, avant de présenter quelques résultats plus récents relatifs à leurs ensembles limites et d’ouvrir la discussion sur leur sensibilité structurelle.

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

This is based on my works with Antoine Spicher and Alexandre Fernandez on so-called “Global Transformations

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.

In most committee-based blockchains, participants propose blocks and then exchange messages, so that a block is accepted if a majority of participants sent the corresponding message.

In this presentation, we will present a game theoretic analysis of committee-based blockchains (which run distributed Byzantine fault tolerant consensus) when participants exhibit strategic or adversarial behaviour. All participants are rational and play best responses. Strategic participants maximize expected net rewards, while adversaries goal is to prevent the consensus.

We show that the prescribed protocol is not an equilibrium, and that there exist equilibria without consensus, even when there are few adversaries. However, under given conditions, there exists an equilibrium satisfying the consensus properties.

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.