Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Agenda
Séminaires antérieurs
Algorithm for Consistent Query Answering under Primary Key Constraints
Speaker: Anantha Padmanabha, ENS Ulm.
Tuesday 10 May 2022, 11:00, (salle 1Z76 ENS Paris-Saclay and online)
Abstract: Databases often have constraints. However, these days it is common to have databases that violate such constraints. Such a database is called an “inconsistent database”. One of the basic constraints is the “primary key constraint” which states there can be at most one tuple for every primary key. If a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q, is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, we have a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete.
The conjecture is open in general, but has been verified for self-join-free and path queries. However, the polynomial time algorithms known in the literature are complex and use different strategies in the two cases. We propose a simple inflationary fixpoint algorithm for consistent query answering which correctly computes certain answers when the query q falls in the polynomial time cases for self-join-free queries and path queries. This raises a natural question, whether this algorithm works for all polynomial time cases. We answer this negatively and show that there are polynomial time certain queries (with self-joins) which cannot be computed by such an algorithm.
This is a joint ongoing work with Diego Figueira, Luc Segoufin and Cristina Sirangelo.
Reaching Consensus in Hostile Environments
Speaker: Thomas Nowak, LISN, Université Paris-Saclay.
Friday 15 April 2022, 11:00, (room 1Z28 ENS Paris-Saclay)
Abstract: Reaching consensus in a distributed system is one of the most fundamental problems studied in distributed computing. It is non-trivial due to uncertainties related to unsuccessful communication and process faults. In particular, the celebrated FLP impossibility result shows why scheduling an event via an asynchronous communication medium such as email is difficult. In this talk, I will present our recent results on exact and approximate consensus in hostile environments such as dynamic networks (e.g., due to mobility of agents) and synthetic bacterial cultures.
Correct Blockchain-based Business Processes
Speaker: Mohamed Graiet, IBM.
Monday April 5th 2022, 11:00, (online)
Abstract: A business process is a chain of events, activities, and decisions intended to achieve a specific organizational goal. Business Process Management (BPM) is a systematic approach to improving these processes.
Blockchain refers to an emerging distributed database technology that relies on a tamper-proof list of timestamped transaction records. Particular attention is paid to the integration of this technology into business processes. This integration makes it possible to create intelligent business processes. In fact, several blockchains are used in several areas, such as cryptocurrency transactions, authenticity, and storage. They provide a way to run processes reliably even in a network without any mutual trust between its nodes. One of the most interesting concepts in blockchain technology is that of smart contracts. A smart contract can be used in the definition of collaborative business processes in general and inter-organizational in particular.
The integration of blockchain technology and business processes still faces complex issues. We are particularly interested in the problem of verifying the correctness of blockchain-based business processes.
Connected multi-agent path finding
Speaker: Francois Schwarzentruber, ENS Rennes and IRISA.
Tuesday March 29 2022, 11:00, (salle 1Z71 ENS Paris-Saclay and online)
Abstract: Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. In the first part of the talk, we study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents. We also introduce a new class called sight-moveable graphs which admit efficient algorithms. In the second part, we discuss conflict-based search and rapidly-exploring random tree.
Weakly unambiguous Parikh automata and their link to holonomic series
Speaker: Florent Koechlin, LORIA.
Monday March 28 2022, 11:00, (room 1Z61 ENS Paris-Saclay and online)
Abstract: I will talk about the connection between inherent ambiguity of formal languages and the properties of their generating series. It is a classical result that regular languages have rational generating series and that the generating series of unambiguous context-free languages are algebraic. In the eighties, Philippe Flajolet developed several tools based on this connection to prove efficiently and easily the inherent ambiguity of many context-free languages, some of which resisted the historical methods based on iterations.
In this talk I will present how these ideas relying on generating series can be extended to Parikh automata, and how they provide an algorithmic tool to decide the inclusion problem for weakly unambiguous Parikh automata. This is a joint work with Alin Bostan, Arnaud Carayol and Cyril Nicaud.
Rational Defeasible Belief Change
Speaker: Ivan Varzinczak, CRIL, Université d'Artois & CNRS, France.
Tuesday March 22 2022, 11:00, (salle 1Z71 ENS Paris-Saclay and online)
Abstract: In this talk, I will present a formal framework for modelling belief change within a non-monotonic reasoning system. Belief change and non-monotonic reasoning are two areas that are formally closely related, with recent attention being paid towards the analysis of belief change within a non-monotonic environment. In this talk, I consider the classical AGM belief change operators, contraction and revision, applied to a KLM-style defeasible setting. The investigation leads us to the formal characterisation of a number of classes of defeasible belief change operators. For the most interesting classes we need to consider the problem of iterated belief change, generalising the classical work of Darwiche and Pearl in the process. This work involves belief change operators aimed at ensuring logical consistency, as well as the characterisation of analogous operators aimed at obtaining coherence, an important notion within the field of logic-based ontologies.
Semantics for Variational Quantum Programming
Speaker: Vladimir Zamdzhiev, Inria
Tuesday 15 March 2022, 11:00, (online)
Abstract: In this talk, I will first introduce myself by briefly summarising my main research activities: (1) formal methods for diagrammatic reasoning about quantum information processing (e.g. higher-order rewriting of ZX-calculus diagrams); and (2) design and analysis of quantum programming languages. I will also explain how this fits perfectly within the research activities of the QuaCS team.
After that I will talk about some recent work on variational quantum programming that will appear in POPL 2022. The technical summary of this talk is below.
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice.
The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.
Proving cryptographic protocols: the complex relationship between symbolic and computation models
Speaker: Guillaume Scerri, Université de Versailles
Tuesday 8 March 2022, 11:00, (salle 1Z34 ENS Paris-Saclay)
Abstract: A number of different models coexist for proving cryptographic protocols. They can roughly be divided in two classes. First, the so called computational model deals with probabilistic Turing machines, precise reductions to specific cryptographic hypotheses often with explicit bounds, and provides very strong guarantees against adversaries that are close to real world. Second the symbolic models, that abstract away probabilities, and model the adversary as a specific list of capabilities. While the computational model provides stronger guarantees, proofs in this model are generally rather complex, hard to check, and not amenable to automation. On the other hand symbolic models typically allow for automated or quasi automated proofs in a much simpler framework. In this talk we will first explore why it is so hard to obtain symbolic models that soundly abstract the computation models. We will then present a fairly recent development, the computationally complete symbolic attacker, developed by Bana and Comon, that takes the opposite approach of usual symbolic models and model what the attacker cannot do rather than modelling the attacker through a list of capabilities. We will explore how this model allows for more modular proofs and proof composition results, and may even allow for efficiently deriving explicit bounds of reductions without ever dealing with the complexity of computational models.
On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows.
Speaker: Damien Busatto-Gaston, Université Libre de Bruxelles (ULB)
Tuesday 15 February 2022, 11:00, (online)
Abstract: In this talk I will present ongoing work on Markov decision processes. Given an MDP and a formula phi, the strategy synthesis problem asks if there exists a strategy for the MDP such that the resulting Markov chain satisfies phi. This challenging problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced globally. Moreover, we allow for linear expressions in the probabilistic inequalities. We show that this class of formulae is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis becomes decidable when strategies are either deterministic or memoryless, while the general problem remains undecidable. We compare with results on the entire PCTL logic and consider applications to the PCTL satisfiability problem.
WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
Speaker: Benjamin Farinier, TU Wien, Austria
Tuesday 25 January 2022, 11:00, (online)
Abstract: The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a compiler turning the Coq model and the Web invariants into SMT-lib formulas.
We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.