TBA

### June 3, 2024

*TBA*

**Federico Olimpieri**

Skip to content
# Seminars 2023-24

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

### June 3, 2024

*TBA*

**Federico Olimpieri**
(University of Leeds)

### May 27, 2024

*TBA*

**Antoine Amarilli**
(LTCI, Telecom-Paris)

### May 13, 2024

*Beyond Decisiveness: When Statistical Verification Meets Numerical Verification*

**Benoît Barbot**
(LACL)

### March 25, 2024

*Bornes inférieures et impossibilité en algorithmique distribuée auto-stabilisante*

**Gabriel Le Bouder**
(LMF, Université Paris-Saclay)

### March 25, 2024

*On the Computability of Compact Sets*

**Djamel Eddine Amir**
(LORIA, Université de Lorraine)

### March 18, 2024

*Mathematical informatics*

**Thomas Seiller**
(CNRS, LIPN)

### March 18, 2024

*Languages of Higher Dimensional Timed Automata*

**Emily Clément**
(IRIF, Université Paris-Cité)

### March 11, 2024

*Lambda-Calculus, Taylor Expansion and (Tropical) Quantitative Semantics: an overview*

**Davide Barbarossa**
(University of Bath)

### March 4, 2024

*Computability of extender sets in multidimensional subshifts*

**Léo Paviet Salomon**
(GREYC, Université Caen Normandie)

### February 26, 2024

*Ingredients for a BSP library*

**Wijnand Suijlen**
(Huawei Technologies)

TBA

TBA

Verification of infinite-state Markov chains is still a challenge despite several fruitful numerical or statistical approaches. For decisive Markov chains, there is a simple numerical algorithm that frames the reachability probability as accurately as required (however with an unknown complexity). On the other hand when applicable, statistical model checking is in most of the cases very efficient. Here we study the relation between these two approaches showing first that decisiveness is a necessary and sufficient condition for almost sure termination of statistical model checking. Afterwards we develop an approach with application to both methods that substitutes to a non decisive Markov chain a decisive Markov chain with the same reachability probability. This approach combines two key ingredients: abstraction and importance sampling (a technique that was formerly used for efficiency). We develop this approach on a generic formalism called layered Markov chain (LMC). Afterwards we perform an empirical study on probabilistic pushdown automata (an instance of LMC) to understand the complexity factors of the statistical and numerical algorithms. To the best of our knowledge, this prototype is the first implementation of the deterministic algorithm for decisive Markov chains and has required to solve several qualitative and numerical issues.

L’auto-stabilisation est un paradigme adapté aux systèmes distribués, particulièrement susceptibles de subir des fautes transitoires. Ces fautes peuvent être des erreurs de corruption de mémoire, de messages, la rupture d’un lien de communication, et peuvent plonger le système dans un état incohérent. Un protocole est auto-stabilisant si, quel que soit l’état initial du système, il garantit un retour à un fonctionnement normal en temps fini.

Avec le développement de réseaux d’objets connectés, censés être autonomes, la question de la conception d’algorithmes tolérants aux pannes ayant un faible coût en termes de consommation énergétique devient cruciale. Une des manières d’appréhender ces problèmes est de chercher à réduire la taille des messages échangés entre les différents nœuds du réseau.

Nous présenterons des résultats négatifs, d’impossibilité et de bornes inférieures pour une famille de problèmes de l’algorithmique distribuée.

The topological properties of a set have a strong impact on its computability properties. A striking illustration of this idea is given by spheres, closed manifolds and finite graphs without endpoints : if a set X is homeomorphic to a sphere, a closed manifold or a such graph, then any algorithm that semicomputes X in some sense can be converted into an algorithm that fully computes X. In other words, the topological properties of X enable one to derive full information about X from partial information about X. In that case, we say that X has computable type. Those results have been obtained by Miller and Iljazović and others in the recent years. We give a characterization of finite simplicial complexes having computable type using a local property of stars of vertices. We argue that the stronger, relativized version of computable type, is better behaved. Consequently, we obtain characterizations of strong computable type, related to the descriptive complexity of topological invariants. This leads us to investigate the expressive power of low complexity invariants in the Borel hierarchy and their ability to differentiate between spaces. Notably, we show that they are sufficient for distinguishing finite topological graphs.

What is a model of computation? What is a program, an algorithm? While theoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomatic consequence is the notion of Turing-completeness. This standard (sole?) equivalence between models of computation is purely extensional: it does only care about what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computation is continuously growing further from how actual machines compute.

I will present a proposal for alternative foundations more faithful to computer science practice and interests. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on *how* computation is performed rather than only on *what* is computed. I will argue that it generalises computability theory while still allowing to recover standard results.

If time permits, I can then explain how this theory can be used to (I will let he audience decide which items will be discussed):

• provide a uniform account of several lower bounds from algebraic complexity and strengthen them

• define static analysis methods which can be implemented in usable tools

• define families of linear realisability models (realisability models for linear logic)

• lead to a semantic approach of implicit computational complexity

• propose a formal definition of the notion of algorithm

• provide a uniform account of several lower bounds from algebraic complexity and strengthen them

• define static analysis methods which can be implemented in usable tools

• define families of linear realisability models (realisability models for linear logic)

• lead to a semantic approach of implicit computational complexity

• propose a formal definition of the notion of algorithm

Higher Dimensional Automata (HDA) are a very powerful tool to represent non-interleaving concurrency (i.e. a || b =/= a.b + b.a). They generalise numerous models, such as Petri nets. Languages of HDA are sets of ipomsets, which represent the possible order on the events.

In recent years, interest in HDAs has increased and has led to numerous new results (e.g. 2021 Fahrenberg et al., 2023: Fahrenberg et al.). Recently, an extension of both Timed Automata and HDA were defined, called Higher Dimensional Timed Automata, to obtain a more refined information on posets: rather than only the precedence order, we are interested in the time intervals in which events are active.

In our work, we define languages of HDTAs as sets of interval-timed pomsets with interfaces. As an application, we show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction, we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable.

The plan of the talk will be, first, to give an overview of the Taylor expansion of the lambda-calculus and, then, to give an overview of some aspects of quantitative categorical semantics.

I will in particular highlight some results obtained for a semantics based on the tropical semiring, which appeared in a recent CSL paper, where programs can be seen as locally Lipschitz functions, and the lambda-calculus Taylor expansion gives local approximants of the Lipschitz constants.

Depending on the interest and the common knowledge of the audience, I will spend more time on one topic or another.

A classical result from the theory of formal languages, the Myhill-Nerode theorem, gives a necessary and sufficient condition in terms of congruence classes for a language to be regular. In this talk, we try to adapt this result to the case of subshifts, in which we consider potentially multidimensional infinite configurations rather than finite words. In particular, we study the behavior of */extender entropy/*, a property introduced by R.Pavlov and T.French which is analogous to congruence classes in formal languages, and obtain some computability characterizations on the possible extender entropies of various classes of subshifts.

The Bulk Synchronous Parallel (BSP) model is a cost model for parallel computation, which algorithm designers can use to estimate how much time their parallel algorithm will take when using multiple processors on their computer simultaneously. Indirectly, it therefore aids also in design of parallel algorithms. The implementation of such a BSP algorithms may be much more complicated, however, because strange interactions inside middle-ware and hardware may unexpectedly ruin the carefully proven complexity bounds. For that reason, various BSP libraries have been proposed and developed, which programmers can use to implement BSP algorithms. This talk presents some of the techniques that such BSP libraries employ in order to present an ordinary computer as a highly reliable and efficient BSP computer.