In collaboration with the logic group of the math department (IMJ-PRG), PPS pole is organizing a meeting:

• Logique à Paris
• 26 - 28 February 2025
• Amphi Turing, Sophie Germain
• https://www.sylvyanscombe.com/logiqueaparis2025.html

Talks are given by six invited speakers on various current topics in logic, which in several cases include interactions with the foundations of computer science: Albert Atserias, Ingo Blechschmidt, Laura Fontanella, Jonathan Kirby, Chris Lambie-Hanson, Mariana Vicaria.

Each speaker will give two hours of lectures; typically, the first lecture gives a broad introduction to their domain, followed by a more in-depth talk on a recent topic.

If you would like to attend one or more of the talks, we kindly request that you register via the link above.

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi 2018) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson 2021), which reduces the hardness of refuting a polynomial equation f(x) = 0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method. This includes hardness over finite fields and hard instances different from Subset Sum variants, both of which were unknown before, and significantly improved constant-depth IPS lower bounds. Conversely, we expose the limitation of this method by showing it cannot lead to proof complexity lower bounds for any hard Boolean instance (e.g., CNFs) for any sufficiently strong proof systems (including AC0[p]-Frege).

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

Duration: two hours.

The plan of the course is:

1. How complex is a graph?
2. First-order Logic
3. Transductions
4. Sparsity I: Measuring shallow minors
5. Sparsity II: Low tree-depth decompositions
6. Sparsity III: Generalized colouring numbers
7. Sparsity IV: Uniform quasi-wideness
8. Graph theory and Logic
9. Limits of graphs I: Classical limits
10. Limits of graphs II: Structural limits
11. Conclusion, Problems, and Discussion

In the $k$-cut problem, we are given an edge-weighted graph and want to find the least-weight set of edges whose deletion breaks the graph into $k$ connected components. Algorithms due to Karger-Stein and Thorup showed how to find such a minimum $k$-cut in time approximately $O(n^{2k-2})$. The best lower bounds come from conjectures about the solvability of the $k$-clique problem and a reduction from $k$-clique to $k$-cut, and show that solving $k$-cut is likely to require time $\Omega(n^k)$. Our recent results have given special-purpose algorithms that solve the problem in time $n^{1.98k + O(1)}$, and ones that have better performance for special classes of graphs (e.g., for small integer weights). In this work, we resolve the problem for general graphs, by showing that for any fixed $k \geq 2$, the Karger-Stein algorithm outputs any fixed minimum $k$-cut with probability at least $\widehat{O}(n^{-k})$, where $\widehat{O}(\cdot)$ hides a $2^{O(\ln \ln n)^2}$ factor. This also gives an extremal bound of $\widehat{O}(n^k)$ on the number of minimum $k$-cuts in an $n$-vertex graph and an algorithm to compute a minimum $k$-cut in similar runtime. Both are tight up to $\widehat{O}(1)$ factors. The first main ingredient in our result is a fine-grained analysis of how the graph shrinks—and how the average degree evolves—under the Karger-Stein process. The second ingredient is an extremal result bounding the number of cuts of size at most $(2-\delta) OPT/k$, using the Sunflower lemma.

We use computers in so many aspects of our lives, from the early days of accounting and calculating trajectories to our use of them for entertainment and communication. The best Human Computer Interaction (HCI) takes the tool out of the task allowing a user to focus on what they are hoping to do. Its all about matching the functional and ergonomic needs of a person without requiring them to learn to much to create their “cognitive model” of how to do things.

Today we are as likely to use a computer while walking down the street as in an office. This talk will touch on classic HCI issues of simplicity focusing also on today’s need to use computers while in social circumstances.

The talk will include discussion of the relationship between functional design engineers attempt to do, aesthetic design graphic artists do, and the cognitive issues that psychologists have found to constrain design as well. Examples of physical graphical and cognitive interface will be described from Ted’s exploration of creating and testing novel interaction scenarios. Emphasis in considerate computing will be highlighted in examples from kitchens to email to automobiles.

A long-standing puzzle in quantum complexity theory is to understand the power of the class MIP* of multiprover interactive proofs with shared entanglement. This question is closely related to the study of entanglement through non-local games, which dates back to the pioneering work of Bell. In this work we show that MIP* contains NEEXP (non-deterministic doubly-exponential time), exponentially improving the prior lower bound of NEXP due to Ito and Vidick. Our result shows that shared entanglement exponentially increases the power of these proof systems, as the class MIP of multiprover interactive proofs without shared entanglement is known to be equal to NEXP.

Over the past ten years, the field of quantum machine learning (QML) has produced many polylogarithmic-time procedures for linear algebra routines, assuming certain “state preparation” assumptions. Though such algorithms are formally incomparable with classical computing, a recent line of work uses an analogous classical model of computation as an effective point of comparison to reveal speedups (or lack thereof) gained by QML. The resulting “dequantized” algorithms assume sampling access to input to speed up runtimes to polylogarithmic in input size.

In this talk, we will discuss the motivation behind this model and its relation to existing randomized linear algebra literature. Then, we will delve into an example quantum-inspired algorithm: Gilyen, Lloyd, and Tang's algorithm for low-rank matrix inversion. This dequantizes a variant of Harrow, Hassidim, and Lloyd's matrix inversion algorithm, a seminal work in QML. Finally, we will consider the implications of this work on exponential speedups in QML. No background of quantum computing is assumed for this talk.

Ali Charara, director of INS2I at CNRS, visits IRIF on the morning of April 24th. The research conducted at IRIF will be presented as well as 6 specific scientific talks.

Vertex connectivity is a classic extensively-studied problem. Given an integer k, its goal is to decide if an n-node m-edge graph can be disconnected by removing k vertices. Although a O(m)-time algorithm was postulated since 1974 [Aho, Hopcroft, and Ullman], and despite its sibling problem of edge connectivity being resolved over two decades ago [Karger STOC'96], so far no vertex connectivity algorithms are faster than O(n^2) time even for k = 4 and m = O(n). In the simplest case where m = O(n) and k = O(1), the O(n^2) bound dates five decades back to [Kleitman IEEE Trans. Circuit Theory'69]. For the general case, the best bound is ~O( min{ kn^2, n^\omega + nk^\omega } ) [Henzinger, Rao, Gabow FOCS'96; Linial, Lovász, Wigderson FOCS'86].

In this talk, I will present a randomized Monte Carlo algorithm with ~O(m + k^3 n) time. This algorithm proves the conjecture by Aho, Hopcroft, and Ullman when k=O(1) up to a polylog factor, breaks the 50-year-old bound by Kleitman, is fastest for 4 < k < n^{0.456}. The story is similar for the directed graphs where we obtain an algorithm running time at most ~O(k^2 m).

The key to our results is to avoid computing single-source connectivity, which was needed by all previous exact algorithms and is not known to admit o(n^2) time. Instead, we design the first local algorithm for computing vertex connectivity; without reading the whole graph, our algorithm can find a separator of size at most k or certify that there is no separator of size at most k “near” a given seed node.

This talk is based on joint works with Danupon Nanongkai and Sorrachai Yingchareonthawornchai.

Dans le contexte des réseaux à grande échelle, la prise en compte des pannes est une nécessité. L’auto-stabilisation est une approche algorithmique de la tolérance aux pannes dans les systèmes distribués dont le but est de gérer la corruption de la mémoire des processeurs dues à des pannes transitoires. Plusieurs paramètres caractérisent l’efficacité d’un algorithme auto-stabilisant, dont en particulier (1) le temps pris par le système pour retourner dans une configuration légale suite à une corruption arbitraire de la mémoire de ses processeurs, et (2) l’espace mémoire utilisé par les processeurs pour exécuter l’algorithme. La minimisation de l'espace mémoire est motivée pas de nombreux aspects : existence de réseaux (tels que les réseaux de capteurs) offrant des espaces mémoires limités, la minimisation des échanges de données entre processeurs voisins, la limitation du stockage d’information afin de pouvoir utiliser des techniques de redondance, etc. Ce séminaire présentera l’auto-stabilisation au travers deux grands problèmes classiques : la construction d’arbres couvrants, notamment d’arbres couvrants de poids minimum, et l’election d'un leader. Il présentera en particulier les liens entre auto-stabilisation et les techniques de décision distribuée, incluant le calcul de bornes inférieures sur l’espace mémoire nécessaire à la résolution par des algorithmes auto-stabilisants des problèmes susmentionnés.

Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. In this talk, I will present some previous work to tackle this problem using reduced hybrid abstractions of the state space explored during the model checking process. Hybrid structures are explicit graphs with symbolic nodes (encoded with symbolic data structures such as decision diagrams). I will illustrate the efficiency of such structures in a general context and show their use to solve some specific problems like diagnosis and opacity checking of discret event systems.

I will review some of my earlier results on work and time complexity of link-reversal routing algorithms, which were introduced by Gafni and Bertsekas in 1981. The theory we developed for the complexity analysis of these algorithms allowed us also to prove that executions of link reversal algorithms on large graphs are similar (a notion which we make precise) to executions on smaller graphs. The latter result has an interesting application to parameterized model checking of a link-reversal-based resource allocation scheme. In particular, we show cases where verification of large systems can be reduced to checking smaller ones.

The observation that distributed algorithm theory has interesting application in computer-aided verification motivated me to explore this connection in more depth. In the second part of the talk, I will present a line of research that in the recent years led to breakthroughs in parameterized model checking of fault-tolerant broadcasting algorithms. I will close the talk by discussing ongoing research lines and open challenges.

The results on link reversal is joint work with Bernadette Charron-Bost, Matthias Fuegger, Antoine Gaillard, and Jennifer Welch. Parameterized model checking of broadcasting algorithms is joint work with Igor Konnov, Marijana Lazic, and Helmut Veith.

Anonymity is a primary ingredient for our digital life. Several tools have been designed to address it, namely blind signatures, group signatures or anonymous credentials for authentication and randomizable encryption or mix-nets, for confidentiality. When it comes to complex electronic voting schemes, random shuffling of ciphertexts with mix-nets is the only known tool and has been largely used in practice, for example in the recent professional election of National Education with more than 430 000 votes. However, achieving anonymity requires huge and complex zero-knowledge proofs to guarantee the actual permutation of the initial ciphertexts.

In this talk, we propose a new approach for proving correct shuffling based on the new notion of extractable linearly-homomorphic signature: the mix-servers can simply randomize individual ballots (meaning the ciphertexts, the signatures, and the verification keys) with an additional global proof of constant size, and the output will be publicly verifiable. The computational complexity for the mix-servers is linear in the number of ciphertexts. It also remains linear in the number of ciphertexts for the verifiers, independently of the number of rounds of mixing. This leads to the most efficient technique of mix-nets, which is at the same time highly scalable.

(Joint work with Hebant Chloé and David Pointcheval)

I will review some of my previous results on code transformations. Everybody knows refactoring that have been widespread by Martin Fowler at the end of the 1990s. A refactoring is a transformation, preserving the behavior of the software system. Such transformations have also the properties to be performed daily and to affect very few entities. At the opposite of the spectrum, there is architecture evolutions that occur once or twice in the software system lifecycle and involve almost the whole system. In between there are a large space for transformations frequently performed almost like refactoring but may impact the behavior. We present two contexts where we applied such transformations.

Le parallélisme synchrone est utilisé aujourd'hui de manière routinière pour concevoir et implémenter le logiciel de controle/commande critique, dans les avions ou les train, par exemple. Il permet d'écrire un modèle mathématique idéal du système en faisant l'hypothèse que tous les processus partagent une échelle de temps globale commune. On raisonne d'abord en négligeant les temps de calculs et de communication, ce qui simplifie la détection de certaines erreurs (interblocages, courses critiques) et les étapes de validation (simulation, test, vérification formelle). Puis on vérifie que le code généré par le compilateur respecte les contraintes de temps d'exécution pire-cas.

Les langages synchrones décrivent des systèmes à temps discret seulement. Ils ne permettent pas de modéliser, ni fidèlement ni très efficacement des systèmes contenant des dynamiques hybrides combinant des signaux à temps discret et à temps continu. Cela créé une rupture dans la chaîne de développement, avec un langage pour la modélisation hybride et un autre pour la modélisation ou l'implémementation du logiciel de contrôle.

Dans cet exposé, nous présenterons Zelus, une extension d'un langage synchrone avec des équations différentielles ordinaires (ODEs) et une opération de détection d'événement (zero-crossing). Il permet d'écrire dans un source unique, un modèle synchrone (à temps discret) du logiciel de controle et un modèle (à temps discret où à temps continu) de son environnement. Nous illustrerons le langage sur quelques exemples. Nous présenterons son système de types qui permet de cloisonner les parties à temps discret et les parties à temps continu pour rejeter des comportements étranges que l'on obtient avec les outils de modélisation hybrides les plus utilisés. Nous montrerons également son analyse par typage des boucles de causalité par typage. Enfin, nous montrerons le principe utilisé pour générer du code séquentiel qui est lié ensuite à un solveur numérique (ici Sundials Cvode). Si le temps le permet, nous discuterons une expérimentation en cours, d'ajout de contructions de programmes probabilistes, ainsi que quelques questions ouvertes autour du typage, de la sémantique et de la vérification.

Les automates cellulaires sont des objets qui peuvent être interprétés, d’un point de vue informatique, comme modèles de calculs parallèles, ou d’un point de vue mathématique, comme systèmes dynamiques. Ils forment donc un pont entre deux domaines de science apparement éloignés. Je donne un bref survol de la théorie des automates cellulaires en dynamique symbolique. Ensuite j’expose deux problèmes différents autour des automates cellulaires auxquels je me suis intéressée.

Le premier problème concerne les propriétés de randomisation de certains automates cellulaires. La randomisation asymptotique est le processus par lequel un état initial de basse entropie est asymptotiquement transformée en un état d'entropie maximale, par l’action itérée de l’automate cellulaire. Je discute des conditions nécessaires et suffisantes pour qu’une telle randomisation survienne, et aussi d'un travail récent avec Eric Rowland.

La deuxième problématique est de caractériser les automates cellulaires qui préservent un langage donné. Je résume un travail récent avec Clemens Muellner, où nous obtenons un théorème de structure pour les automates cellulaires qui préservent certains langages HD0L.

Algorithms are one of the most fundamental elements in computer science. Networks and networked systems are no exception. In this talk, I will present our recent research on some algorithmic problems of both fundamental and practical importance in modern networks and networked systems, more specifically, wireless networks. Methodologically, most of our analysis is systematically articulated as follows: (1) Establishment of theoretical performance bound, (2) Optimum or approximation algorithm design, (3) Further extension and generalization. Our objective is to make a tiny while systematic step forwards in the design and analysis of algorithms that can scale elegantly, act efficiently in terms of computation and communication, while keeping operations as local and distributed as possible.

After giving a brief introduction to quantum evolutions, whether finite (automata) or infinite-dimensional (operators), I will explore their impact upon computability and universality. Most of the results I will mention rely on a decomposition of quantum operators into quantum 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.

The set of all integer partitions admits the structure of a graded lattice, called Young lattice, which leads to a beautiful proof for the correspondence between pairs of Young tableaux of the same shape and factorial numbers. All this is due to the fact that this lattice is a differential poset, property introduced by Stanley. A generalization of this property has been provided by Fomin through graded graph duality. Some families of combinatorial objects admit such structures, and the counting of some Hasse walks reveal a nice combinatorics. We present here a new concept of graph duality, pairs of graded graphs of trees, and their lattice properties. We also show how to construct pairs of graded graphs from operads. This allows us to recover existing graphs (like the composition poset or the bracket tree) and to discover new ones.

An important problem in theoretical computer science is to determine whether two programs are equivalent. For instance, this is needed to determine whether the optimizations performed by a compiler actually preserve the meaning of the input programs. For lambda calculi, it has become standard to consider two programs as equivalent whenever they can be plugged in any context without noticing any difference in their behavior. Such notion of equivalence depends on the behavior one is interested in observing. We provide syntactic and semantic characterizations of the equivalence arising by taking as observables the beta normal forms, corresponding to completely defined values. As a byproduct we obtain characterizations of the different degrees of extensionality in the theory of Böhm trees.

The last few years have seen a surge of decision problems with an astronomical, non primitive-recursive complexity, in logic, verification, and games. While the existence of such uncontrived problems is known since the early 1980s, the field has matured with techniques for proving complexity lower and upper bounds and the definition of suitable complexity classes. This framework has been especially successful for analysing so-called `well-structured systems'—i.e., transition systems endowed with a well-quasi-order, which underly most of these astronomical problems—, but it turns out to be applicable to other decision problems that resisted analysis, including two famous problems: reachability in vector addition systems and bisimilarity of pushdown automata.

In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. The decidability of the problem was first shown by Mayr thanks to a decomposition algorithm. I will present succinctly the main ideas behind a tight Ackermannian complexity upper bound obtained with Jérôme Leroux for this algorithm.

The talk will start with presenting a brief overview of querying incomplete information in databases and the main computational challenges it presents. Querying incomplete data invariably relies on the very coarse classification of query answers into those that are certain and those that are not. Such a classification is often very costly, and we propose to refine it by measuring how close an answer is to certainty.

This measure is defined as the probability that the query is true under a random interpretation of missing information in a database. Since there are infinitely many such interpretations, to pick one at random we adopt the approach used in the study of asymptotic properties and 0-1 laws for logical sentences and define the measure as the limit of a sequence. We show that in the standard model of missing data, the 0-1 law is observed: this limit always exists and can be only 0 or 1 for a very large class of queries. Thus, query answers are either almost certainly true, or almost certainly false, and this classification behaves very well computationally. When databases satisfy constraints, the measure is defined as the conditional probability of the query being true if the constraints are true. This can now be an arbitrary rational number, which is always computable. Another refinement of the notion of certainty views answers with a larger set of interpretations that make them true as better ones. We pinpoint the exact complexity of finding best answers for first-order queries.

The collaborative construction of a blockchain is the core of Bitcoin protocol for allowing various participants to agree on a list of valid transactions. The talk will be very informal, the intent is to give a very basic introduction on how Bitcoin works and highlight some of the scientific challenges behind it.

Up-to techniques are a well-known method for accelerating proofs of

behavioural equivalences between systems. In this talk, I 
introduce up-to techniques for behavioural metrics in a coalgebraic
setting and provide general results that show under which conditions
such up-to techniques are sound.

For a system modelled as a coalgebra for a certain functor, the
behavioural distance can be seen as a coinductive predicate using a
suitable lifting of the functor. I will focus on the so called
Wasserstein lifting of a functor for which we provide a new
characterization in a fibrational setting. This is useful for
automatically proving the soundness of up-to techniques via a
generic framework developed in a previous CSL-LICS'14 paper.

I will use  fibrations of predicates and relations valued in a
quantale, for which pseudo-metric spaces are an example. To
illustrate our framework I provide an example on distances between
regular languages.

The module is a continuation of the lecture series by Prakash Panangaden on Labelled Markov Processes, but can be independently followed.

The module is a continuation of the lecture series by Prakash Panangaden on Labelled Markov Processes, but can be independently followed.

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”