Séminaires

May 22 10:30 ₂₀₂₆

Abstract: Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this talk, we will discuss this problem for the theory of Presburger Arithmetic. We will show that Presburger Functional Synthesis (PFnS) can be solved in EXPTIME, and discusss a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Read more...

Jun 17 14:00 ₂₀₂₆

Abstract: This talk highlights some of the most fascinating aspects of the logic of hybrid games, which constitute the foundation for developing multi-agent cyber-physical systems (CPS) such as robots, cars and aircraft, with the mathematical rigor that their safety-critical nature demands. Differential game logic (dGL) provides an integrated specification and verification language for hybrid games that combine discrete transitions and continuous evolution along differential equations with adversarial dynamics resolved by different players with different objectives. dGL can be used to study the existence of winning strategies for hybrid games, i.e., ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e., one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic.

In addition to providing a strong theoretical foundation for CPS, differential game logic as implemented in the KeYmaera X prover has been instrumental in verifying the multi-aircraft dynamics of the Federal Aviation Administration's Airborne Collision Avoidance System ACAS X and constitutes the foundation for control envelope synthesis in hybrid systems.

References:

André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0

André Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. DOI:10.1145/2817824

André Platzer. Differential hybrid games. ACM Trans. Comput. Log. 18(3), pp. 19:1-19:44, 2017. DOI:10.1145/3091123

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.

Read more...

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.