~~NOCACHE~~ /* DO NOT EDIT THIS FILE */ [[en:seminaires:gel:index|Graphs and Logic]]\\ Wednesday April 30, 2025, 1:30PM, Salle 1021\\ **Sylvain Schmitz** (IRIF) //Well quasi-orders and preservation theorems for First-Order Logic - Part II// \\ Continuation of part I. I intend to cover - applications of WQOs in algorithmic graph theory, - a focus on classes of graphs that are well-quasi-ordered by the induced subgraph ordering, along with Pouzet’s Conjecture, - the generalisation to preservation properties in first-order logic. [[en:seminaires:topos:index|Topos Theory]]\\ Wednesday April 30, 2025, 2PM, Salle 3052\\ **Umberto Tarantino** //Elementary topoi (chapter IV)// [[en:seminaires:pps:index|Proofs, programs and systems]]\\ Friday May 2, 2025, 10:30AM, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\ **Quantale-Valued Modal Logic** (Chapman University) //Alexander Kurz// \\ For applications of logic it is often desirable to have a common umbrella encompassing both classical discrete two-valued and quantitative continuous many-valued reasoning.  What are principled ways to extend 2-valued modal logic to many-valued modal logic? What is a suitable generalization of Kripke semantics to this setting? We will explain how category theory allows us to build a general framework to answer these questions. The key observation is that 2 is not only the familiar Boolean algebra but also an instance of a more general structure known as a quantale. A quantale is simply a complete lattice with a little extra structure. As observed by Lawvere in 1973, this extra structure allows us to extend ordinary 2-valued logic to a generalized logic that takes truth values in an arbitrary quantale. The models of such generalized logics encompass a variety of structures including (generalized partial) metric spaces. In this talk, we will give an introduction to this area of logic and also sketch some novel results about canonical extensions of fuzzy-algebras obtained in collaboration with Apostolos Tzimoulis. [[en:seminaires:algocomp:index|Algorithms and complexity]]\\ Monday May 5, 2025, 11AM, Salle 3052\\ **Ryu Hayakawa** (Kyoto University) //Quantum and classical complexities in the homology of higher-order networks// \\ The algorithm and computational complexity of problems in higher-order networks i.e., higher-dimensional extensions of graphs, gather attention due to a successive application of algebraic topology especially in topological data analysis. Surprisingly, it has recently been revealed that the "homological problems" (e.g. find a high-dim hole) in higher-order networks possess quantum computational complexity. In this talk, I show exponential quantum computational speedup results for such a problem. I also discuss a class of higher-order networks where the problem falls into classical complexity. [[en:seminaires:programmation:index|Programming]]\\ Monday May 5, 2025, 10AM, 3071\\ **Timothy Bourke** (INRIA) //Une interface entre OCaml et la bibliothèque Sundials des solveurs numériques// \\ Résumé : Dans le cadre d'un projet de recherche sur les langages de programmation pour les systèmes hybrides, autour du langage Zelus (https://zelus.di.ens.fr), nous avons développé la bibliothèque Sundials/ML (https://inria-parkas.github.io/sundialsml/) pour interfacer OCaml avec les structures de données et les algorithmes du logiciel Sundials développé à Lawrence Livermore National Laboratories. Nous nous sommes efforcés de créer une interface complet, efficace et proche de celui proposé aux programmeurs C, tout en voulant exploiter le système de types et les fonctionnalités d'OCaml (types algébriques de données, fonctions d'ordre supérieur, exceptions, gestion automatique de la mémoire). Le partage de données entre OCaml et C s'avère particulièrement délicat dans ce contexte où un fil d'exécution peut se faufiler entre les deux langages. Certaines de nos solutions pour ce problème sont satisfaisantes, d'autres moins. Nous en présenterons quelques-unes. [[en:seminaires:automates:index|Automata]]\\ Friday May 9, 2025, 2PM, Salle 3052\\ **Quentin Aristote** (IRIF) //Learning automata weighted over number rings, concretely (and categorically)// \\ We study automata weighted over number rings, that is, rings of integers in an algebraic number field. We show that number rings are what we call "almost strong Fatou": if an n-state automaton weighted in a number field recognizes an integer-valued series, then it admits an equivalent n+1-state automaton weighted in the corresponding ring of integers. We give a polynomial-time algorithm for computing such an n+1-state automaton, and show that removing any more states is at least as hard as solving the principal ideal problem, for which the best currently known algorithm is in quantum polynomial time. Finally, we will see how this procedure can be used to reduce active learning problems in number rings to active learning problems in fields. If time allows, I will also give a brief teaser of how this generalizes to a generic reduction procedure between active learning problems for automata valued in different categories. These categorical aspects will be further developed on May 15th for a talk at the AutCat seminar. [[en:seminaires:verif:index|Verification]]\\ Monday May 12, 2025, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\ **Jeroen Keiren** (Eindhoven University of Technology) //An Expressive Timed Modal Mu-Calculus for Timed Automata// \\ In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such as TCTL. Yet, the state of the art of timed mu-calculi is underdeveloped. In this talk, I present a timed model mu-calculus $L_{rel}^{\mu,\nu}$ for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. Additionally, I establish that, in contrast to other timed mu-calculi, $L_{rel}^{\mu,\nu}$ is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for $L_{rel}^{\mu,\nu}$ are immediately usable as model checkers for TCTL for general timed automata. This is joint work with Rance Cleaveland and Peter Fontana, and appeared as [1]. [1] Cleaveland, R., Keiren, J.J.A., Fontana, P.: An Expressive Timed Modal Mu-Calculus for Timed Automata. In: Hillston, J. et al. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems., pp. 160–178. Springer Nature Switzerland, Cham (2024). [[en:seminaires:numeration:index|One world numeration seminar]]\\ Tuesday May 13, 2025, 2PM, Online\\ **Artem Dudko** (IM PAN) //On attractors of Fibonacci maps// \\ In 1990s Bruin, Keller, Nowicki, and van Strien showed that smooth unimodal maps with Fibonacci combinatorics and sufficiently high degree of a critical point have a wild attractor, i.e. their metric and topological attractors do not coincide. However, until now there were no reasonable estimates on the degree of the critical point needed. In the talk I will present an approach for studying attractors of maps, which are periodic points of a renormalization. Using this approach and rigorous computer estimates, we show that the Fibonacci map of degree $d=3.8$ does not have a wild attractor, but that for degree $d=5.1$ the wild attractor exists. The talk is based on a joint work with Denis Gaidashev. [[en:seminaires:doctorants:index|Non-permanent members' seminar]]\\ Thursday May 15, 2025, 4PM, Salle 3052\\ **Lucas Pouillart** //To be announced.// [[en:seminaires:automates:index|Automata]]\\ Friday May 16, 2025, 2PM, Salle 3052\\ **Lê Thành Dũng (Tito) Nguyễn** (LIS (Marseille)) //The structure of polynomial growth for tree automata/transducers and MSO set queries// \\ Given an ℕ-weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorithm that computes the exact polynomial degree of growth in cubic time. As a special case, they apply to the growth of the ambiguity of a nondeterministic tree automaton, i.e. the number of distinct accepting runs over a given input. Our time complexities match the recent fine-grained lower bounds for these problems restricted to ambiguity of word automata. We deduce analogous decidability results (ignoring complexity) for the growth of the number of results of set queries in Monadic Second-Order logic (MSO) over ranked trees. In the case of polynomial growth of degree k, we also prove a reparameterization theorem for such queries: their results can be mapped to k-tuples of input nodes in a finite-to-one and MSO-definable fashion. This has several consequences for transducers, that I will probably not have the time to cover in the talk, but you can check out the preprint: https://arxiv.org/abs/2501.10270 (joint work with Paul Gallot and Nathan Lhote).