Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Agenda
Séminaires antérieurs
On the edit distance between transducers
Speaker: C. Aiswarya, CMI
Wednesday, 19 April 2023, 16:00, 1Z56 ENS Nord and Zoom
Abstract: Given a metric over words, define the distance between two transducers with identical domain as the supremum of the distances of their respective outputs over all inputs. This is a useful generalisation for comparing transducers that goes beyond the equivalence problem. Two transducers are said to be close (resp. k-close) if their distance is bounded (resp. at most k). We will discuss the decidability of the problem that asks whether two given transducers are close (resp. k-close), for common edit distances.
This is a joint work with Amaldev Manuel and Saina Sunny.
Aiswarya will be at LMF from 2 April to 2 June 2023 as a Visiting Professor of ENS Paris-Saclay.
String constraints with subword ordering: complexity of satisfiability
Speaker: C. Aiswarya, CMI
Monday, 17 April 2023, 15:00, Salle 1Z14 and Zoom
Abstract: We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. The satisfiability problem for this variant turns out to be undecidable. We consider a fragment in which the subword-order constraints do not impose any cyclic dependency between variables. We show that this fragment is \nexptime-complete. As an application of our result, we settle the complexity of control state reachability in acyclic lossy channel pushdown systems, which was shown to be decidable in Atig-Bouajjani-Touilli-08. We show that this problem is \nexptime-complete.
This is a joint work with Prakash Saivasan and Soumodev Mal, which appeared in LICS 22.
Aiswarya will be at LMF from 2 April to 2 June 2023 as a Visiting Professor of ENS Paris-Saclay.
The Future of Model-based Testing
Speaker: Jan Peleska, Universität Bremen, Saarbrücken, Germany
Friday 17 March 2023, 14:00, Room 1Z56
Abstract: Since the 1970s, model-based testing (MBT) has been comprehensively investigated in the research communities, and its industrial application has been fostered for at least two decades. Though convincing success stories about MBT have been published, we have to admit that its acceptance in industry is still not as good as it should be. This is reflected, for example, by the facts that commercial MBT tools are not selling as well as had been originally envisaged by the “campaigners of MBT” (such as myself) and that MBT has not been integrated into the verification plans of the key players in the embedded systems world. Read more...
Strategy Complexity of Zero-Sum Games on Graphs
Speaker: Pierre Vandenhove
Tuesday, 14 Mars 2023, 14:00, 1Z77
Abstract: In this seminar, I will present the results obtained as part of my PhD thesis cosupervised by Patricia Bouyer at LMF and Mickael Randour at Université de Mons (Belgium). This seminar precedes my thesis defense which will take place in Mons in April. I include here a short abstract; more details are available at my website.
We study zero-sum turn-based games on graphs. Such games can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. The synthesis problem consists in automatically building a controller for the system that guarantees a given objective no matter what happens in the environment, that is, a winning strategy in the derived game.
A Gentle Introduction to Matching Logic and its Applications
Speaker: Dorel Lucanu
Wednesday, 29 March 2023, 14:00, Salle 1Z56, hybrid
Abstract: Matching Logic (ML) allows to uniformly specify and reason about programming languages and properties of their programs. It was developed as a logical foundation of the K framework.
ML is expressive enough to specify all properties within various logical systems such as FOL, separation logic, lambda-calculus, (dependent) type systems, and modal mu-calculus. In particular, it supports operational semantics (term rewriting) and axiomatic semantics (Hoare triples). ML has a sound fixed Hilbert-style proof system that supports formal reasoning for all specifications. In this talk we give a gentle introduction to (Applicative) Matching Logic [3], we show how the initial algebraic semantics can be encoded as ML theories [4], and how ML is used to formaly define programming languages semantics and program properties.
The Frobenius Anatomy of Distributed Quantum Protocols
Speaker: Alexis Toumi, email: alexis@toumi.email
Tuesday, 10 January 2023, 14:00, Salle 1Z31
Abstract: Distributed consensus and leader election are two communication problems that quantum computers can solve in a deterministic way, while classical computers can only solve them probabilistically. These two quantum protocols can in fact be put in one-to-one correspondance with the GHZ and W states, the only two ways to entangle three qubits (up to LOCC, local operations and classical communication). In this talk, we will give an abstract formulation of quantum consensus and leader election in terms of spiders, also known as Frobenius algebras. In both cases, a single equation allows to create global entanglement from local interactions: spider fusion. We will conclude with some applications to quantum natural language processing (QNLP) where spiders allow to formalise the notion of anaphora and co-reference: we can compute a global meaning for text as the entanglement of local meanings for sentences.
An Abstraction of the Unit Interval with Denominators
Speaker: Marco Abbadini
Wednesday, 4 January 2023, 14:00, visio link: https://zoom.us/j/97278780690?pwd=cGU5Yi9UVTk0aXhndWtuanY4dHp0QT09
Abstract: Compact Hausdorff spaces are the topological abstraction of the unit interval [0,1] (in a sense that can be made precise). Let us now equip the unit interval with the "denominator map" den: [0,1] -> N that maps a rational number to its denominator and an irrational number to 0. We characterize the abstraction of [0,1] that takes into account both the topology and the denominator map.
(We use this result to provide a representation theorem for a class of lattice-ordered groups, generalizing a result of M.H. Stone (1941).)
Keynote: The Skolem Landscape
Speaker: Joël Ouaknine, Max Planck Institute for Software Systems, Saarbrücken, Germany
Tuesday, 13 December 2022, 14:00, Room 1Z56
Abstract: The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, the decidability of the Skolem Problem has been open for nearly a century! In this talk, I will present a survey of what is known on this problem and related questions, including recent and ongoing developments.
Consistent Circuits for Indefinite Causal Order
Speaker: Augustin Vanrietvelde, LMF
Tuesday, 6 December 2022, 14:00, Room 1Z53
Abstract Over the past decade, a number of quantum processes have been proposed which are logically consistent, yet feature a cyclic causal structure. However, there exists no general formal method to construct a process with an exotic causal structure in a way that ensures, and makes clear why, it is consistent. Here we provide such a method, given by an extended circuit formalism. This only requires directed graphs endowed with boolean matrices, which encode basic constraints on operations. Our framework (a) defines a set of elementary rules for checking the validity of any such graph, (b) provides a way of constructing consistent processes as a circuit from valid graphs, and (c) yields an intuitive interpretation of the causal relations within a process and an explanation of why they do not lead to inconsistencies. We display how several standard examples of exotic processes, including ones that violate causal inequalities, are among the class of processes that can be generated in this way; we conjecture that this class in fact includes all unitarily extendible processes.
Programming with (Discrete and Continuous) Ordinary Differential Equations
Speaker: Olivier Bournez, LIX, École Polytechnique
Tuesday, 15 November 2022, 14:00, Room 1Z14
Abstract: Initially motivated by understanding the computational power of various continuous-time analog models of computations, several characterizations of complexity and computability classes have been obtained recently using ordinary differential equations. Basically, each class is characterized as the class of functions containing some basic functions, and closed by composition and various natural schemas or constructions, based on ordinary differential equations.
This means for one direction of these proofs that we can program with ordinary differential equations.
We will provide a review of some of these recent results, and some applications. We will mainly focus on their discrete counterpart, also known as discrete ordinary differential equations, or finite differences.