First Order Coalition Logic : Model Checking, Complétude et Satisfaisabilité
Davide Catta (LIPN, Paris 13)
June 25, 2025
Les logiques pour le raisonnement stratégique constituent une vaste famille d’outils formels conçus pour modéliser, vérifier et analyser les capacités et les stratégies (individuels ou collectifs) d’agents autonomes, dans un environnement compétitif.
Nous introduisons First Order Coalition Logic (FOCL), qui combine les intuitions de Coalition Logic (CL) et de Strategy Logic (SL). Plus précisément, FOCL permet une quantification arbitraire sur les actions de groupes d’agents.
Dans cet exposé, nous montrons que FOCL est strictement plus expressive que d’autres logiques de coalition connues, puis nous discutons de sa procédure de model checking. Ensuite, nous fournissons une axiomatisation cohérente et complète de cette logique, qui est, à notre connaissance, la première axiomatisation d’une logique stratégique dans la littérature. Enfin, nous montrons que le problème de la satisfaisabilité est indécidable.
Author: lmvadm
[June 2025] Five members of the LMV Team at the Journées Nationales du GdR GPL & Journées AFADL
These national conference are in Pau from June 16 to June 19. Myriam Clouet presents her work Monday at 2PM, Jordan Ischard presents his work on Tuesday at 11:50AM, Frédéric Loulergue gives a keynote Wednesday at 9AM, Terence Clastres presents his poster and Frédéric Dabrowski chairs the CLAP session on Thursday afternoon.
[May 2025] Flo Groult reaches the regional final of MT180
Congratulations Flo! 5 episodes present the preparation to this competition (in French): https://www.youtube.com/watch?v=5eZzsvt8XDk and the final is there: https://www.youtube.com/watch?v=i1SIfkADv8c (Flo’s presentation starts at 38′)
[May 2025] Welcome to Paul Nicolas, Thomas Theault & Mohamed Haady Tiemtore
Mohamed, Paul and Thomas join the LMV team for a BSc internship in May-July 2025
[April 2025] Talk by Leandro Gomes
An algebraic approach for union bound reasoning about probabilistic programs
Leandro Gomes, Université de Lille, CRIStAL
April 10, 2025
[February 2025] Several positions available in the LMV Team
Check out the Job page!
[January 2025] Talk by Loïc Sylvestre
Eclat : un langage synchrone pour la programmation sûre, expressive et efficace de circuits FPGA
Loïc Sylvestre, Sorbonne Université, LIP6
January 27, 2025
[November 2024] Talk by Thibaut Benjamin
Mechanisation of computation for identity types in Martin-Löf type theory
Thibaut Benjamin (University of Cambridge)
November 25, 2024
Martin-Löf type theory is a powerful theory that is at the foundation of modern proof assistants such as Coq, Lean, Agda. It provides a unifying framework to formalise mathematics and software. Although this framework is powerful enough to formalise and verify very complex software (like for instance the CompCert C compiler, formally verified in Coq), its practical use is constrained by the large proof effort it requires, rendering the adoption of such tools slower. Various techniques are considered to simplify and streamline the use of proof-assistants. For instance, identity types, that represent equalities have a very rich and complex structure, and it is common to ignore that structure by adding a principle called Uniqueness of Identity Proofs (UIP). This axiom states that any two identity proofs are equal thus enforcing in a way proof irrelevance for equality. Another example is the so-called univalent axiom (originally coming from a connection with homotopy theory) that for computer scientists mean that the formalisation can be done in a way that is independent of the choice of datatypes, as long as those datatypes encode the same information. This is not only a powerful reasoning principle that allows one to reason on simple but inefficient datatypes and transport the results to finicky but efficient ones, it also reflects the very common computer science practice of hiding the implementation of datatypes under an API to make the programs more modular. Unfortunately, UIP and the univalence axiom are incompatible. In this talk, I will present a workflow that I am designing to handle and automate complex computation on identity types, in an effort to reduce the need for UIP and render practical the use of the univalence axiom. I will in particular show the implementation of this workflow as a Coq plugin, that uses a secondary tool called CaTT, which is specifically designed to handle the algebraic structure of identity types, called higher groupoid.
[November 2024] Poste de MCF dans l’équipe LMV au concours 2025
[November 2024] Frédéric Dabrowski defended his HDR
Congratulations!