Séminaires

Mar 24 14:00 ₂₀₂₆

Abstract: Psychological theories are often incompletely specified—that is, certain cases are overlooked, and some statements are ambiguous or imprecise. This is largely due to the fact that such theories are rarely expressed using formal models. Yet in many scientific disciplines, formal modeling plays a crucial role in theory-building: it enhances the precision of predictions, strengthens scientific reasoning, and facilitates collaboration. We propose two automata-based frameworks and a methodology for modeling psychological theories—that is, for transforming informal, verbal descriptions into formal, analyzable models.

These frameworks use communicating finite automata, along with a refinement procedure for theory-building, as well as model-checking to verify that a model is faithful to the original theory. We prove the pseudo-inclusion of traces of the refinement procedure, as well as a completeness property of our framework.

This method highlights theoretical ambiguities and inconsistencies, and prompts research questions. We illustrate our method using Lazarus and Folkman’s theory of stress as well as the consciousness theory called the Global Neuronal Workspace hypothesis. We provide a step-by- step formalization of these theories.

Jun 9 13:00 ₂₀₂₆

Training session with Alain Finkel, Raphael Faure, Gaspard Fougea, and Stéphane Le Roux, that will take place at ENS Paris-Saclay. Registration is free but mandatory. Click here to register.

Here are three videos that explain the framework we use to model psychological theories with formal models:

Introduction to the framework (1 minute 20)

An overview of the tools we use (7 minutes 20)

A short example of modeling (5 minutes)

This framework is also useful for the modeling of neuro-cognitive theories.

Abstract: The replicability crisis stems partly from a lack of formal models in psychology. In many scientific disciplines, formal modeling plays a crucial role in theory-building: it enhances the precision of predictions, strengthens scientific reasoning, and facilitates collaboration. In this workshop, we introduce a computational framework and methodology for stepwise translating verbal psychological theories into formal models, as well as for verifying the faithfulness of these models to the original theories. This approach leverages tools from theoretical computer science to support theory development, modular design, formal verification, and comparative analysis.

This framework is designed to be both fully formal, with precise mathematical definitions and properties, and easy to grasp through intuitive visual representations. Applying it to a verbal theory highlights theoretical ambiguities and inconsistencies, and prompts research questions.

The workshop is designed as a hands-on introduction to this framework. Participants will be invited to bring a verbal theory from their own research and will be guided in translating it into a formal model. We will teach participants how to extract concepts and developments from the verbal theory and how to use refinement operations to model them.

We propose a four-hour format in which we will: explain the framework and methodology by providing an example; apply it to a new theory collectively; help participants apply it individually in groups of two or three with our support; and then help them identify new research questions that emerged from the modeling.

Dec 9 14:00 ₂₀₂₅

Abstract: An important question in the domain of distributed computing is that of task solvability : given a distributed task, the analog of a program specification for distributed systems, under which conditions can it be solved by some distributed protocol ? The topological approach to distributed computing represents tasks and protocols as relations between simplicial complexes, combinatorial objects which encode possible global states of the system. These have a spatial interpretation, which led to the Asynchronous Computability Theorem (ACT), which relates, for certain computational models, the existence of a continuous map to task solvability, using subdivisions of the input space.

Read more...

Dec 2 14:00 ₂₀₂₅

Abstract:I am interested in verification of distributed systems with an unbounded number of agents running the same finite-state program. These include systems like conservative Petri nets, population protocols, reconfigurable broadcast networks and more. Properties of interest for these systems are "parameterized": for example, is there a number of agents N such that my system instantiated with N agents reaches a bad configuration? I will present a recent result on HyperLTL for population protocols, where we will see that the verification problem can be cast as a parameterized reachability property. I will then present some open questions for parameterized verification of such systems. If I have time, I will present my newest research direction which concerns runtime verification of distributed systems, and the hypotheses that can be made on the setting.

Nov 18 14:00 ₂₀₂₅

Abstract:For better or worse, some mathematicians working in formalisation (including myself) like to work in a proof-relevant setting, such as HoTT or simply MLTT without UIP. While theorems stated in these settings enjoy interpretations in a rich class of models, this matters little if we can't prove them. Indeed, even when proving the most innocent-looking theorems, there is one recurring issue that often stumps even the most seasoned formaliser: coherences. This talk is about my most recent visit to coherence hell and, in particular, a neat little trick that helped me and my collaborators escape it.

More specifically, this talk concerns an ongoing formalisation project with Tom de Jong and Nicolai Kraus on so-called Leibniz products and exponentials (also known as pushout products and pullback powers) and their adjointness. Although this problem is motivated by the development of simplicial type theory, it is also completely self-contained and should be understandable to anyone who knows some basic MLTT and/or category theory. The approach we've taken provides a heuristic for dealing with many coherence problems in general and my hope is that it will be useful to mathematicians and computer scientists stuck on similar problems.

Oct 28 14:00 ₂₀₂₅

Abstract:We give an introduction to higher-dimensional automata (HDAs) and their languages and evoke some of their many nice properties: a Kleene theorem, a Myhill-Nerode theorem, and a BET theorem. We also show how HDAs may be applied in the analysis of Petri nets and, if time permits, will delve into real-time extensions.

Jun 10 14:00 ₂₀₂₅

Abstract:

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step, such that the LTL formula is satisfied. In this talk, we investigate the notion of dependent outputs in the context of reactive synthesis. Inspired by successful pre-processing techniques in Boolean functional synthesis, we define dependent outputs in reactive synthesis as outputs that are uniquely determined, given an assignment to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent outputs. Using this, we show that dependent outputs are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel framework that exploits dependent outputs in solving a synthesis problem. By implementing this framework using the widely used library Spot, we show that reactive synthesis that exploits dependent variables can solve some problems beyond the reach of existing techniques. Furthermore, we observe that among benchmarks with dependent outputs, if the count of non-dependent variables is low (≤ 3 in our experiments), our method outperforms state-of-the-art tools for synthesis.

This is joint work with S. Akshay, Eliyahu Basa and Dror Fried, and appeared in TACAS 2024.

Bio:

Supratik Chakraborty is Bajaj Group Chair Professor of Computer Science and Engineering at IIT Bombay. His research interests lie at the intersection of theoretical and applied computer science, with a focus on scalable and practical formal methods. He is a Fellow of Indian National Academy of Engineering and a Distinguished Member of ACM.

May 20 14:00 ₂₀₂₅

Abstract:

I present three case studies from my collaborative research that highlight the essential role of logic in enhancing our understanding of modern machine learning architectures. The first two examples focus on the expressive capabilities of two prominent architectures: Transformers, which have revolutionized NLP applications, and Graph Neural Networks, a leading approach for classifying graph-structured data. We employ temporal logic techniques to analyze the properties that Transformers can recognize, and modal logics to examine the properties discernible by Graph Neural Networks. The third example addresses the pursuit of explainable AI, demonstrating how first-order logic can be used to design languages that declare, evaluate, and compute explanations for decisions made by machine learning models.

Apr 29 14:00 ₂₀₂₅

Abstract:

Regular word grammars are context-free grammars having restricted rules, that define all recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier ``regular'' is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.

This is joint work with Marius Bozga (Verimag) and Florian Zuleger (TU Wien).

Mar 4 14:00 ₂₀₂₅

Abstract: Tamarin-prover is a tool for symbolic modeling and analysis of security protocols. It takes as an input a protocol's model, specifying the roles of the different agents (initiator, responder, different attacker models...) and some security properties required by the protocol. Tamarin can simulate an unbounded number of sessions running in parallel, which means an infinite number of role instances and possible fresh numbers. The execution of the different roles gives a transition system. The security properties are written as trace properties that will be matched against the transition system. To conduct proofs, Tamarin includes by default eight static heuristics. They help cover most cases, but can sometimes be really inefficient. In order to deal with these cases, Tamarin allows its users to create personalized heuristics by writing a script in a foreign programing language (usually python). However, this functionality has several limits (limited input information, state agnostic, compatibility issues). Moreover, while going through the proof tree, Tamarin can get stuck in a loop which prevents the proof from finishing. In this presentation, I will present several tools and approaches to improve Tamarin termination, from a new heuristic language to loop detection and bounded explorations for attack finding. I will also show how these new tools can be combined for greater results.

Mar 11 14:00 ₂₀₂₅

Abstract:

Alpha-beta pruning is an efficient search strategy for two-player game trees. It was invented in the late 1950s and is at the heart of most implementations of combinatorial game playing programs. In this talk I will survey my recent formalizations and verifications of a number of standard variations of alpha-beta pruning. Findings include:

• Basic variants already having a property ascribed to an improved version
• Authors being confused about which algebraic structure they actually work in
• Generalizations to new algebraic structures
• The implementation in a famous paper is flawed

Read more...