Logics for Strategic Reasoning: Recent Developments and Application to Mechanism Design

Speaker: Munyque Mittelmann, University of Naples

Tuesday, 12 December 2023, 14:00, Room 1Z71

Abstract: In recent years a wealth of logic-based languages have been introduced to reason about the strategic abilities of autonomous agents in multi-agent systems. This talk presents some of these important logical formalisms, namely, the Alternating-time Temporal Logic and Strategy Logic. We discuss recent extensions of those formalisms to capture different degrees of satisfaction, as well as to handle uncertainty caused by the partial observability of agents and the intrinsic randomness of MAS. Finally, we describe the recent application of those formalisms for Mechanism Design and explain how they can be used either to automatically check that a given mechanism satisfies some desirable property, or to produce a mechanism that does it.


Séminaires antérieurs

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

Speaker: Raphael Berthon, RWTH Aachen

Tuesday, 28 November 2023, 14:00, Room 1Z25

Abstract: When verifying multiple properties, it is sufficient to verify each individually, but when synthesizing strategies that satisfy multiple objectives, these objectives must be considered together. We consider the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single omega-regular objective expressed as parity that must be surely met while satisfying n reachability objectives with some probability thresholds too. We consider three combinations with a sure parity objective: (a) strict and (b) non-strict thresholds on all reachability objectives, and (c) maximizing the thresholds under a lexicographic ordering on the reachability objectives. We highlight the notion of projection for combining multiple objectives. We show that the decision variants of (a) are in PTIME, (b) in EXPTIME, and (c) can be solved by considering n parity games, and give associated algorithms.

Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Speaker: Farzad Jafarrahmani, IRIT

Tuesday, 21 November 2023, 14:00, 1Z56

Abstract: The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (\muMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this talk, I present an extension of the phase semantics of multiplicative additive linear logic (a.k.a. \MALL) to \muMALL with explicit (co)induction (i.e. \muMALLind). Then I introduce a Tait-style system for \muMALL where proofs are wellfounded but potentially infinitely branching. We will see its phase semantics and the fact that it does not have the finite model property. This presentation is based on joint work with Abhishek De and Alexis Saurin.

Analysis of Parameterized Systems

Speaker: Chana Weil-Kennedy, Technical University Munich

Tuesday, 19 December 2023, 14:00, to be announced

Abstract: My research project focuses on parameterized verification of distributed systems, where the parameter is often the number of agents present in the system. During my thesis with Javier Esparza in Munich, I studied this kind of problem for subclasses of Petri nets with application to population protocols, but also for systems communicating by broadcast or by shared register. Currently in my postdoc I am continuing the study of these systems with "simple" modes of communication, and I'm also starting to look at language inclusion problems. In the future, I want to continue to analyze distributed systems for which the parameterized problems are not immediately undecidable, by broadening the range of formal method techniques used.

The Church Synthesis Problem Over Continuous Time

Speaker: Alex Rabinovich, Tel Aviv University

Tuesday, 14 November 2023, 14:00, Room 1Z56

Abstract: Church’s Problem asks for the construction of a procedure which, given a logical specification φ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an operator F that implements the specification in the sense that φ(I, F(I)) holds for all inputs I. Büchi and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

Partially commuting pushdowns and rational trace relations

Speaker: Dietrich Kuske, Technische Universität Ilmenau

Tuesday, 5 September 2023, 14:00, Room 1Z34

We consider the reachability problem for pushdown systems where the pushdown does not store a word, but a Mazurkiewicz trace. Since this model generalizes multi-pushdown systems, the reachability problem can only be solved for a restricted class that we call cooperating multi-pushdown systems (cPDS). In the talk, I will show how the saturation algorithm by Finkel et al. (1997) can be modified. For such saturated cPDS, the reachability relation can be shown to be a finite union of finite compositions of prefix-recognizable trace relations (for words, these relations were studied, e.g., by Caucal, 1992).


Some challenges in quantum computing for linear algebra algorithms and data structures

Speaker: Marc Baboulin, Université Paris-Saclay

Tuesday, 12 September 2023, 14:00, Room 1Z34

Quantum computing aims at addressing computations that are currently intractable by conventional supercomputers but it is also a promising technology for speeding up some existing simulations. However it is commonly accepted that quantum algorithms will be essentially ``hybrid'' with some tasks being executed on the quantum processor while others will remain treated on classical processors (CPU, GPU,...). Among the crucial tasks achieved on classical computers, several require efficient linear algebra algorithms.


Building a Provenance-Aware Database Management System

Speaker: Pierre Senellart, ENS Ulm, head of the Valda joint CNRS, ENS, Inria project-team

Tuesday, 4 July 2023, 10:30, 1Z14

We describe ProvSQL, software currently being developed in our team that adds support for provenance management to a regular database management system, PostgreSQL. We first explain what provenance is, applications thereof, and how provenance of database queries can be defined and captured. We insist on one particular application of provenance, probabilistic query evaluation. We then explain research and engineering challenges in implementing techniques from the scientific literature on provenance management and probabilistic databases within a major database management system.

Formal Proofs for Trajectory Computation in the Plane with Straight Obstacles

Speaker: Yves Bertot, INRIA Antipolis

Tuesday, 4 July 2023, 9:20, 1Z14

Our goal is to describe smooth trajectories for robots, so that these robots don't have to stop to change direction. Several formats of trajectories could be used, but we decided to focus on trajectories given by Bézier curves. It happens that these curves have mathematical properties that make it easy to verify formally that there are no collisions. Work in collaboration with Quentin Vermande (ENS, Paris) and Reynald Affeldt (AIST, Tokyo, Japan).

Keynote: Verification of Stateful Security Protocols in Isabelle/HOL

Speaker: Achim Brucker, Chair of Computer Security, University Exeter, GB

Tuesday May 16 2023, 14:00, Room 1Z61

Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation.

While many typical components like the security protocol TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure.

The verification of security protocols is one of the success stories of formal methods. There is a wide spectrum of methods available, ranging from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. Read more...

Minimal Generating Sets for Semiflows

Speaker: Gerard Memmi LTCI, Telecom-Paris, Institut polytechnique de Paris

Tuesday, 23 Mai 2023, 14:00, Room 1Z56 and Zoom

We discuss important characteristics of finite generating sets for F+, the set of all semiflows with non-negative coordinates of a Petri Net. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature and also to better position the re- sults while considering semirings such as N or Q+ then fields such as Q. As accurately as possible, we provide a range of new algebraic results on minimal semiflows, minimal supports, and finite minimal generating sets for a given family of semiflows. Minimality of semiflows and of sup- port are critical to develop effective analysis of invariants and behavioral properties of Petri Nets. Main results are concisely presented in a table and our contribution is highlighted. We conclude with the analysis of an example drawn from the telecommunication industry underlining the efficiency brought by using minimal semiflows of minimal supports.