• Login

en fr

Friday Seminar Seminar series of the teams Formal Methods for Artificial Intelligence, Distributed Computing, and Model-Checking & Synthesis

Organizers: Patricia Bouyer-Decitre, Stéphane Demri, Matthias Függer

Format

The seminar brings together the teams Formal Methods for Artificial Intelligence, Distributed Computing, and Model-Checking & Synthesis to share research ideas in a relaxed and open setting. Talks cover ongoing work, recent results, and topics of interest to the three groups. Sessions are one hour and speakers are encouraged to aim for 45 minutes to leave ample time for discussion which we consider an essential part of this series. The seminar values informal presentation style and lively interaction. Seminars take place Fridays at 14h00.

Upcoming talks

Previous talks

% reserved: June 12th: Rustam Galimullin @next{Luc26, author={Luc Lapointe}, institution= {LMF}, homepage={https://home.lmf.cnrs.fr/LucLapointe/}, title={A three sides problem about graphs, tilings and concurrent games}, abstract={}, datum={10 April 2026 14:00}, note={Room 1Z53} } @next{Rustam26, author={Rustam Galimullin}, institution= {University of Bergen}, homepage={https://rgalimullin.gitlab.io/}, title={TBC}, abstract={TBC}, datum={12 June 2026 14:00}, note={Room 1Z77} } % ======= 2026 ======= @talk{Nowak26, author={Thomas Nowak}, institution={LMF}, homepage={https://www.thomasnowak.net/}, title={Vibe Formalizing: Having AI Agents Lean-Prove Our Paper}, abstract={We report on an ongoing experiment in which we use AI coding agents to formally verify proofs from a recent paper in Lean 4, without prior experience in Lean or interactive theorem proving. The workflow pairs two agents: one generates Lean proofs by running the compiler in a feedback loop, while the other checks that the formalizations faithfully correspond to the paper's statements. Using this setup, we have so far formalized several results, including formalization of computational models. We will demonstrate the workflow, show where it works well, where it fails, and discuss the bottlenecks we encountered.<br />Teaser: <a href="https://youtube.com/shorts/wi494CWAz1A">youtube.com/shorts/wi494CWAz1A</a>}, datum={27 March 2026 14:00}, note={Room 1Z53}, } @talk{Shibashis26, author={Shibashis Guha}, homepage={https://www.tifr.res.in/~shibashis.guha/}, institution= {Tata Institute of Fundamental Research, India}, title={Optimising Expectation with Guarantees for Window Mean Payoff in Markov Decision Processes}, abstract={The window mean-payoff objective strengthens the classical mean-payoff objective by computing the mean payoff over a finite window that slides along an infinite path. Two variants have been considered: in one variant, the maximum window length is fixed and given, while in the other, it is not fixed but is required to be bounded. In this work, we look at the problem of synthesising strategies in Markov decision processes that maximise the window mean-payoff value in expectation, while also simultaneously guaranteeing that the value is above a certain threshold. We solve the synthesis problem for three different kinds of guarantees: sure (that needs to be satisfied in the worst-case, that is, for an adversarial environment), almost-sure (that needs to be satisfied with probability one), and probabilistic (that needs to be satisfied with at least some given probability p).<br />   We show that for the fixed window mean-payoff objective, when the window length is given in unary, all the three problems are in polynomial time, while for the bounded window mean-payoff objective, they are in both NP and coNP, and thus have the same complexity as for maximising the expected performance without any guarantee. Moreover, we show that pure finite-memory strategies suffice for maximising the expectation with sure and almost-sure guarantees, whereas, for maximising expectation with a probabilistic guarantee, randomised strategies are necessary in general.<br />   This is a joint work with Pranshu Gaba.}, datum={20 March 2026 14:00}, note={Room 1Z76}, } @talk{GuyAvni26, author={Guy Avni}, homepage={https://sites.google.com/view/gavni}, institution={University of Haifa}, title={Bidding Games}, datum={2 March 2026 14:30}, note={Room 1Z56}, } @talk{Orna26, author={Orna Kupferman}, homepage={https://www.cs.huji.ac.il/~ornak/}, institution={Hebrew University of Jerusalem}, title={History-Deterministic Automata}, datum={2 March 2026 13:30}, note={Room 1Z56}, } @talk{Alain26, author={Alain Finkel}, homepage={https://lmf.cnrs.fr/AlainFinkel/}, institution= {LMF}, title={Psychology 101 for Students}, datum={6 Feb 2026 14:00}, note={Room tba}, } % ======= 2025 ======= @talk{Ghosh25, author={Arka Ghosh}, homepage={https://www.mimuw.edu.pl/~arka/}, institution= {Warsaw University & LaBRI, Bordeaux}, title={Equivariant polynomial ideals and their membership problem}, abstract={For an infinite set X (of variables) and a group G acting on X, an ideal J in the polynomial ring K[X] in X over the field K is called equivariant (w.r.t. G) if J is invariant under the action of G. We give a necessary and sufficient condition on the action of G on X for the following extension of Hilbert's basis theorem: every equivariant ideal in K[X] is finitely generated. We also prove that this condition implies decidability of the equivariant ideal membership problem: given a polynomial f and finite set of polynomials H, decide whether f is in the equivariant ideal generated by H. These results in particular imply decidability of the zeroness problem of weighted register automata, of the universality problem of unambiguous register automata without guessing, and of the reachability problem of reversible data Petri nets for a wide range of data domains.<br /> This is joint work with Sławomir Lasota and Aliaume Lopez.}, datum={12 Dec 2025 14:00}, note={Room tba}, } @talk{Fervari25, author={Raul Fervari}, homepage={https://rfervari.github.io/}, institution= {FAMAF-UNC and CONICET, Argentina, and LMF, U. Paris-Saclay, France}, title={On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories}, abstract={In this talk I will present an extension of Linear Time Temporal Logic (LTL) with past operators, featuring modalities to perform local updates on the models. Such structures are infinite sequences of valuations interpreting variables by elements from a possibly infinite data domain. Some particularly interesting examples include the Boolean domain, the natural numbers, the integers, and the rational numbers, to name a few. I will introduce some expressivity and complexity results for our LTL variants performing updates over concrete domains, and some general ideas about their proofs.<br /> This talk is based on the recent paper: S. Demri and R. Fervari. On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025), pages 260–270. 2025.}, datum={5 Dec 2025 14:00}, note={Room tba}, } @talk{Guillou25, author={Lucie Guillou}, homepage={https://lucieguillou.github.io/}, institution= {IRIF}, title={Wait or Act: Parameterized Verification with Wait-Only Protocols and Non-Blocking Communication}, abstract={I will present my PhD thesis which falls within the framework of formal verification of parameterized distributed/concurrent systems, in which an unbounded number of identical processes execute the same program and interact via two communication mechanisms: (1) non-blocking rendez-vous: a process sends a message that is instantly received by another process, and if no process is ready to receive the message, it is simply lost (but still sent). (2) broadcast: a process sends a message received simultaneously by all processes capable of receiving it. Verifying these systems then amounts to do so for all possible numbers of processes. Hence, we obtain an infinite number of systems, which makes usual model checking methods to verify such systems impossible. In this context, we study several problems of parameterized verification. In this presentation, I will talk about state coverability (can a process reach a particular state?), configuration coverability (can the system evolve towards a configuration that covers a target configuration?), and synchronization (can all processes reach the same state simultaneously?). We show that the state and configuration coverability problems are ExpSpace-complete in networks where processes communicate only with the non-blocking rendez-vous mechanism, improving a previous result that only demonstrated decidability. On the other hand, we show that the synchronization problem is undecidable. Our main contribution consists of introducing Wait-Only protocols, a syntactic restriction where each state is either a waiting state (unable to receive any message) or an action state (unable to perform any emission of message). We obtain a fundamental property called the copypaste property, which guarantees that if an action state and another state are separately coverable, then they are also coverable together. For this class, we prove that some verification problems enjoy a significant reduction in complexity compared to the general case.}, datum={28 Nov 2025 14:00}, note={Room tba}, } @talk{Mascle25, author={Corto Mascle}, homepage={https://corto-mascle.github.io/}, institution= {MPI-SWS}, title={The Short-Ends Factorisation Theorem and applications}, abstract={This talk aims to advertise a new method for factorising words with respect to a finite monoid. The approach lets us represent a word as a tree of bounded size relative to the monoid, where long sequences of contiguous factors that induce the same effect in the monoid are abstracted by retaining only the first and last few. We will explore three a priori unrelated problems and show how they are connected to one another and to the short-ends factorisation method. The talk will focus on presenting those connections rather than describing the solutions. The first problem concerns the parameterised control of populations of MDPs. The second is the sequential flow problem, which asks whether it is possible to compose sequences of graph fragments in order to generate graphs with unbounded max-flow. The third problem is the computation of the subword closure of the language generated by an indexed grammar. For each of these problems, we establish optimal bounds.}, datum={21 Nov 2025 14:00}, note={Room tba}, } @talk{Berthon25, author={Raphaël Berthon}, homepage={https://moves.rwth-aachen.de/people/raphael-berthon/}, institution= {LMF}, title={A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games}, abstract={Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. We introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. This work was presented at CONCUR 2025}, datum={14 Nov 2025 14:00}, note={Room tba}, } @talk{Vialard25, author={Isa Vialard}, homepage={https://isavialard.github.io/home/}, institution= {MPI-SWS}, title={(Un)decidability of the Value problem for Two-clock Weighted Timed Games}, abstract={The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs has remained stubbornly open for a decade. We recently shown its undecidability. However, the Value problem is decidable for a subclass of two-clock weighted timed games.}, datum={17 Oct 2025 14:00}, note={Room tba}, } @talk{Shenwald25, author={Noam Shenwald}, homepage={https://noamshenwald.github.io/}, institution= {Hebrew University of Jerusalem}, title={Coverage Games}, abstract={We introduce and study coverage games -- a novel framework for multi-agent planning in settings in which a system operates several agents but does not have full control on them, or interacts with an environment that consists of several agents. The game is played between a coverer, who has a set of objectives, and a disruptor. The coverer operates several agents that interact with the adversarial disruptor. The coverer wins if every objective is satisfied by at least one agent. Otherwise, the disruptor wins. Coverage games thus extend traditional two-player games with multiple objectives by allowing a (possibly dynamic) decomposition of the objectives among the different agents. They have many applications, both in settings where the system is the coverer (e.g., multi-robot surveillance, coverage in multi-threaded systems) and settings where it is the disruptor (e.g., prevention of resource exhaustion, ensuring non-congestion). We study the theoretical properties of coverage games, including determinacy, and the ability to a priori decompose the objectives among the agents. We solve the problems of deciding whether the coverer or the disruptor wins, analyze their tight complexity, and consider useful special cases.}, datum={10 Oct 2025 14:00}, note={Room tba}, } @talk{Bu25, author={Burkhart Wolff}, homepage={https://usr.lmf.cnrs.fr/~wolff/}, institution= {LMF}, title={HOL-CSP - A Comprehensive Formal Theory of Concurrency}, abstract={In this overview talk, I present the theory architecture in Isabelle/HOL that evolved over the last years. The key issue is to present a framework that reconciles the data- and behavior dimension in concurrency with a proof-theory based on solid foundations. The architecture starts with a denotational semantics for CSP and its extensions, an algebraic theory using fixed-point Induction permitting the reasoning over infinite data sets, a symbolic operational Semantics, techniques to reason over process-architectures as well as connections to deterministic and non-deterministic infinite automata and model-checking. Finally, we sketch applications coming from the domain of autonomous systems. This presentation attempts a synthesis of the work of Safouan Taha, Lina Ye, Benoit Ballenghien, Benjamin Puyobro, Adrien Durier and myself.}, datum={12 Sep 2025 14:00}, note={Room 1Z61} } @talk{Mic25, author={Vincent Michielini}, homepage={https://vimichielini.com/}, institution= {University of Warsaw, Poland}, title={Query Entailment Problem for S}, abstract={In description logic, possibly infinite structures are described via an ABox A (i.e. a basic finite structure, to be completed), and an ontology T (or a TBox, a finite set of constraints aiming to complete the ABox). The query entailment problem asks the following: given an ABox A, a TBox T, and a conjunctive query q (= a subgraph), does any structure satisfying A and T necessarily also satisfy the request? In ALC, the basic description logic (which is nothing more than modal logic in disguise), this problem is well understood, as it is known to be ExpTime-complete in combined complexity, and coNP-complete in data complexity (i.e. with TBox and query fixed) [Lutz '08]. However, the exact complexity for S, the extension of ALC where some roles (= binary relations) are specified to be transitive, was not known yet. The status being that the problem is coNExpTime-hard [Eiter et al. '09] and in 2ExpTime [Calvanese et al. '98]. Two articles in 2009 and 2010 tried to close the gap by proving coNExpTime-completeness in special cases, but the general question remained open. In this seminar, we finally answer this question by showing that the query entailment problem for S is actually 2-ExpTime complete. In fact, we show that the complexity gap is associated with the number of transitive roles: two distinct transitive roles are enough to get 2-ExpTime-hardness, while the case with only one transitive role (and possibly many non-transitive ones) is in coNExpTime. This latter case is proven by showing that whenever q is not entailed by (A,T), then there exists a counterexample with a representation of exponential size (while being most certainly infinite). In the talk, we will explain how some variant of automata over infinite trees can be elegantly used in order to obtain such a representation. We will also highlight the crucial difficulties induced by two distinct transitive roles, that were overlooked so far. }, datum={28 March 2025 11:00}, note={Room 1Z56} } @talk{youssouf25, author={Youssouf Oualhadj}, homepage={https://www.lacl.fr/~youalhadj/}, institution= {LACL}, title={Robust timed synthesis}, abstract={Solving games played on timed automata is a well-known problem and has led to tools and industrial case studies. In these games, the first player (Controller) chooses delays and actions and the second player (Environment) resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. Finally we present a notion "repair" where we explain how to recover robustness in non-robust systems.}, datum={28 March 2025 14:00}, note={online} } @talk{Ligozat25, author={Anne-Laure Ligozat}, institution={LISN & ENSIIE}, homepage={https://perso.limsi.fr/annlor/}, title={Empreinte environnementale de l'IA : quelles méthodes et résultats ?}, datum={28 March 2025 15:30}, note={Room 1Z56}, } @talk{Fioravantes25, author={Foivos Fioravantes}, institution={Czech Technical University in Prague}, homepage={https://sites.google.com/view/foivos-fioravantes/}, title={Recent advances in exact algorithms for the Multiagent Path Finding problem}, datum={24 March 2025 11:00}, note={online}, } @talk{janna25, author={Janna Burman}, homepage={https://www.lisn.upsaclay.fr/membres/burman-janna/}, institution= {LISN}, title={Distributed Computing despite Failures and Limited Resources}, abstract={Many nowadays emerging networks, as well as nature inspired or biological systems are intended to operate under harsh and even hostile environments. They may be prone to failures and dispose of very few resources. Such systems are typically decentralized, dynamically changing and asynchronous in nature. Their entities may be limited in terms of memory, energy and may have poor communication or computational capabilities. In this talk, we describe some of our recent work on the algorithmic foundations of such distributed systems. We use an analytical approach based on formal models, i.e., on formal representation of the system network, reflecting its capacities. Such models allow proving the correctness of a solution, determining the limits between feasibility and impossibility and detecting performance bottlenecks. We focus on three distributed computing models: population protocols, mobile agents and the beeping model. They address different types of resource limitations, in particularly in terms of memory and communication capabilities. Their computing entities cooperate for solving fundamental distributed problems such as leader election, counting, synchronization or exploration. We design efficient algorithms for these problems, especially aiming at uniform, deterministic and self-stabilizing (tolerating transient failures) solutions. Efficiency is justified by optimal time and memory complexities.}, datum={21 March 2025 11:00}, note={Room 1Z56} } @talk{uli25, author={Uli Fahrenberg}, institution= {LRE}, title={Petri nets, concurrency, and real time}, abstract={Petri nets and their variants are often considered through their interleaved semantics, i.e. considering executions where, at each step, a single transition fires. This is clearly a miss, as Petri nets are a true concurrency model. We revisit the semantics of Petri nets as higher-dimensional automata (HDAs) as introduced by van Glabbeek, which methodically take concurrency into account. We extend the translation to include inhibitor arcs, under both concurrent semantics used in the literature, in the process introducing partial HDAs. Finally, we also consider time Petri nets and propose a semantics based on higher-dimensional timed automata (HDTAs), and show how common constructions and results from timed automata may be lifted to HDTAs. }, datum={21 March 2025 16:00}, note={Room 1Z14} } @talk{Mouna25, author={Mouna Safir}, institution= {LIP6}, title={k-set agreement in Distributed systems}, abstract={Distributed systems consist of collaborating processes and form the foundation of many modern services, ranging from online banking to social media. A central challenge in these systems is achieving consensus among all computers or processes. This challenge is addressed by agreement algorithms, which play a crucial role in ensuring the proper functioning of a distributed system. These algorithms help maintain consistency and reliability within the system. In this presentation, I will focus on the k-agreement problem. This problem is a generalization of the conventional consensus problem, centering on reaching an agreement among processes, where the agreement is limited to at most k values, with k=1 corresponding to consensus. The task becomes complex when some processes fail—either by crashing (terminating execution prematurely and permanently) or by behaving unpredictably. The latter are known as Byzantine behaviors. The objective is to clarify the conditions under which the k-agreement problem can be solved and to define its resolution limits. A key achievement of my research is the near-complete mapping of the resolution of the k-agreement problem. Through novel and improved algorithms, we have enhanced the efficiency of k-agreement, particularly in environments characterized by Byzantine behaviors and constrained message transmission delays. These environments are modeled within Byzantine synchronous message-passing systems, which may or may not include authentication. While our primary interest was in Byzantine synchronous message-passing systems, we also explored asynchronous environments, characterized by unpredictable message transmissions and potential process failures. Here, we extended solutions to address these challenges, bridging gaps left by previous studies. In summary, our study provides a comprehensive analysis of k-agreement within Byzantine synchronous message-passing systems, offering innovative and optimal algorithms.}, datum={14 March 2025 11:00}, note={Room 1Z14} } @talk{Etienne25, author={Étienne André}, institution= {Université Sorbonne Paris Nord}, title={Monitoring cyber-physical systems under uncertainty}, abstract={Monitoring cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals gathered in a log, while real behaviors are continuous-time signals, which implies some uncertainty. In addition, the monitoring properties can themselves feature some uncertainty: e.g., a period in a property to be monitored can be uncertain or even unknown. In this presentation, we present two ways to address uncertainty while monitoring cyber-physical systems. First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds. We rely on two solutions, one based on model-checking, and the other one being ad-hoc. Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)---the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log. We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant.}, datum={14 March 2025 14:00}, note={Room 1Z56} } @talk{aline25, author={Aline Goeminne}, homepage={https://alinegoeminne.github.io/}, institution= {ENS Rennes, IRISA}, title={A stroll with multiplayer reachability games}, abstract={One of the most elementary objective studied in games played on a finite directed graph is the reachability objective. In its qualitative variant, a player with a qualitative objective only aims at reaching a given subset of vertices, called his target set. When weights are assigned to the edges of the game graph, the particular case of quantitative reachability objective may be studied. Roughly speaking, a player equipped with such an objective wants to minimize the cumulative weights until a vertex of his target set is reached. In this talk, we consider multiplayer games played on graphs such that all players have a qualitative or a quantitative reachability objective. The most famous solution concepts studied in multiplayer games are those of equilibria, e.g., Nash equilibria (NEs) and subgame perfect equilibria (SPEs). In the first part of this talk, we consider decision problems related to the existence of NEs or SPEs with some constraints on the players' objectives. We are interested in deciding the existence of an equilibrium such that: (in the qualitative setting) a given subset of players have to reach their target set; or (in the quantitative setting) players have to reach their target set within a given number of steps. Exact characterizations of the set of outcomes of NEs (resp. SPEs) allow to prove that these problems are NP-complete (resp. PSPACE-complete). In the second part of the talk, we focus only on qualitative reachability games and move from the classical notion of a player's strategy to the concept of multi-strategy. A multi-strategy for Player i prescribes a set of possible actions when it is Player i's turn to play, instead of a single action. Thus, once a multi-strategy is fixed for each player, there are several paths in the game graph that are consistent with these multi-strategies from a given initial vertex. In this setting, we aim at synthesizing the most permissive multi-strategies. The permissiveness of two multi-strategies can be compared with penalties, as already used in the two-player zero-sum setting by Bouyer et al. [1]. Once the notions of permissive NE and SPE are properly defined, we show that we can decide the existence of a permissive equilibrium, while satisfying some upper-bound constraints on the penalties in PSPACE, if the upper-bound penalties are given in unary. The same holds when we search for a permissive equilibrium where certain players are asked to win in at least one consistent play or in all consistent plays. [1] Patricia Bouyer, Marie Duflot, Nicolas Markey, Gabriel Renault: Measuring Permissivity in Finite Games. CONCUR 2009.}, datum={7 March 2025 11:00}, note={Room tba} } @talk{svg25, author={Sam van Gool}, homepage={https://www.samvangool.net/}, institution= {LMF, CNRS & ENS Paris-Saclay}, title={Separation, duality, and profinite lambda calculus}, abstract={TBA}, datum={21 February 2025 11:00}, note={Room tba} } @talk{lav25, author={Laetitia Laversa}, homepage={https://l-laversa.github.io/}, institution= {IRIF, U. Paris-Cité}, title={Execution-time opacity control for timed automata}, abstract={TBA}, datum={14 February 2025 11:00}, note={Room tba} } @talk{cle25, author={Émily Clément}, homepage={https://perso.eleves.ens-rennes.fr/people/emily.clement/}, institution= {IRIF}, title={Logic and language results for concurrent models}, datum={31 January 2025 11:00}, abstract={For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. In this talk, I explain my recent works regarding these models and its timed version. Temporal logics are a powerful tool to specify properties of computational systems. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In recent work, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp's theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp's theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no auto-concurrency. In previous work, we worked on lifting decidability and undecidability results from Timed Automata to a timed version of HDA, Higher Dimensional Timed Automata.}, note={Room 1Z71} } @talk{Kniazev25, author={Roman Kniazev}, institution={LaBRI, Université de Bordeaux}, homepage={https://roman.knzv.me}, title={Programmatic Reinforcement Learning: why and how?}, datum={24 January 2025 11:00}, note={Room 1Z71}, } @talk{sam25, author={Andrew Samokish}, institution= {LMF}, title={A graphical modeling framework arKItect as a tool for structuring and federating system data}, abstract={The Knowledge Inside company has developed an innovative hybrid data federation technology that bridges the gap between modeling and databases through the use of Domain-Specific Modeling Languages. The cornerstone of arKItect's design lies in its implementation of the recursive "System of Systems" concept. Leveraging a low-code paradigm, arKItect enables intuitive model definition, complemented by default recursive graphical representations. The primary objective of the talk is to formalize the underlying approach and explore ways to extend the applicability and versatility of the resulting models. }, datum={17 January 2025 11:00}, note={Room 1Z71} } % ======= 2024 ======= @talk{Demri24b, author={Stéphane Demri}, institution={LMF, CNRS}, homepage={https://cv.hal.science/stephane-demri}, title={How to manage a budget with ATL+}, abstract={Paper: <a href="https://proceedings.kr.org/2023/19/">proceedings.kr.org/2023/19/</a>}, datum={25 October 2024 11:00}, note={Room 1Z61}, } @talk{mas24, author={Corto Mascle}, institution= {LaBRI, U. Bordeaux}, title={Synthesis of distributed systems with locks and variables}, abstract={I will start with a study of the controller synthesis problem for a model in which a finite set of processes communicate using locks and variables. Although this problem is generally undecidable, we discuss restrictions that allow us to achieve decidability. Specifically, we require that processes acquire and release locks in a nested fashion, similar to how items are managed in a stack, and limit the number of times a process switches while writing to variables. Then, I will present ongoing work and open questions concerning the verification and synthesis of distributed systems, with a particular focus on dynamic and parameterised settings.}, datum={15 October 2024 10:00}, note={Room 2U47} } @talk{gui24, author={Quentin Guilmant}, homepage={https://www.mpi-sws.org/people/guilmant/}, institution= {MPI-SWS}, title={Inaproximability in Weighted Timed Games}, abstract={We consider two-players, turn-based weighted timed games played on timed automata equipped with (positive and negative) integer weights, in which one player seeks to reach a goal location whilst minimising the cumulative weight of the underlying path. Although the value problem for such games (is the value of the game below a given threshold?) is known to be undecidable, the question of whether one can approximate this value has remained a longstanding open problem. In this paper, we resolve this question by showing that approximating arbitrarily closely the value of a given weighted timed game is computationally unsolvable. This is achieved via a reduction to a problem shown undecidable in 1989 by Condon and Lipton about (separated) probabilistic automata.}, datum={11 October 2024 11:00}, note={Room 1Z61} } @talk{cas24, author={Antonio Casares}, homepage={https://antonio-casares.github.io/}, institution= {University of Warsaw, Poland}, title={Positional omega-regular languages}, abstract={In the context of infinite duration games over graphs, a central question is: For which objectives can the existential player always play optimally using positional (memoryless) strategies? We characterize omega-regular objectives with this property, obtaining decidability in polynomial time and answering a conjecture by Kopczyński. The automata-constructions introduced in this work are the starting point for the definition of canonical models of parity automata. This is joint work with Pierre Ohlmann. }, datum={4 October 2024 11:00}, note={Room 1Z61} } @talk{gossner24, author={Olivier Gossner}, homepage={http://gossner.me}, institution={CNRS, Ecole Polytechique, LSE}, datum={6 September 2024, 11:00}, note={Room 1Z18}, title={A Discrete Language for Higher-Order Interactive Decision Making}, abstract={While language is usually thought of as a discrete process, beliefs, as well as beliefs over beliefs, etc. are captured by higher and higher level continuous spaces.We show how, by focusing on player’s choices in a given game, all hierarchies of beliefs can be represented through a discrete model embedded into a finite automaton. The talk presents results from the paper "Rationalizable Outcome Distributions: A Markov Characterization" with Rafael Veiel, available at <a href="http://gossner.me/wp-content/uploads/2023/01/rationalizable.pdf">gossner.me/.../rationalizable.pdf</a>} } @talk{guh24b, author={Shibashis Guha}, homepage={https://www.tifr.res.in/~shibashis.guha/}, institution= {Tata Institute of Fundamental Research (TIFR), Mumbai}, title={A Game of Pawns}, abstract={We introduce and study pawn games, a class of two-player zero-sum turn-based graph games. A turn-based graph game proceeds by placing a token on an initial vertex, and whoever controls the vertex on which the token is located, chooses its next location. This leads to a path in the graph, which determines the winner. Traditionally, the control of vertices is predetermined and fixed. The novelty of pawn games is that control of vertices changes dynamically throughout the game as follows. Each vertex of a pawn game is owned by a pawn. In each turn, the pawns are partitioned between the two players, and the player who controls the pawn that owns the vertex on which the token is located, chooses the next location of the token. Control of pawns changes dynamically throughout the game according to a fixed mechanism. Specifically, we define several grabbing-based mechanisms in which control of at most one pawn transfers at the end of each turn. We study the complexity of solving pawn games, where we focus on reachability objectives and parameterize the problem by the mechanism that is being used and by restrictions on pawn ownership of vertices. On the positive side, even though pawn games are exponentially-succinct turn-based games, we identify several natural classes that can be solved in PTIME. On the negative side, we identify several EXPTIME-complete classes, where our hardness proofs are based on a new class of games called Lock & Key games, which may be of independent interest. Joint work with Guy Avni, and Pranav Ghorpade}, datum={28 June 2024 14:00}, note={Room 1Z14} } @talk{guh24a, author={Shibashis Guha}, homepage={https://www.tifr.res.in/~shibashis.guha/}, institution= {Tata Institute of Fundamental Research (TIFR), Mumbai}, title={Strategy synthesis for global window PCTL}, abstract={Given a Markov decision process (MDP) M and a formula Phi, the strategy synthesis problem asks if there exists a strategy sigma such that the resulting Markov chain M[sigma] satisfies Phi. This 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 all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is shown to be decidable when strategies are deterministic while the problem is undecidable for arbitrary strategies. Joint work with Benjamin Bordais, Damien Busatto-Gaston, and Jean-François Raskin }, datum={21 June 2024 14:00}, note={Room 1Z14} } @talk{Cortal24, author={Gustave Cortal}, institution={LMF}, homepage={https://lmf.cnrs.fr/Perso/GustaveCortal}, title={Statistical Language Modeling: From N-grams to Transformers}, datum={31 May 2024 11:00}, note={Room 1Z18}, abstract={Recorded talk: <a href="https://www.youtube.com/watch?v=PenKM-gZX_4">youtube.com/watch?v=PenKM-gZX_4</a><br />Slides: <a href="https://gustavecortal.com/data/Gustave_Cortal_Tutorial_on_Language_Models.pdf">gustavecortal.com/.../Language_Models.pdf</a>}, } @talk{gab24, author={Pranshu Gaba}, homepage={https://pranshugaba.com/}, institution= {Tata Institute of Fundamental Research (TIFR), Mumbai}, title={Stochastic Window Mean-payoff Games}, abstract={Stochastic two-player games model systems with an environment that is both adversarial and stochastic. The environment is modelled by a player (Player 2) who tries to prevent the system (Player 1) from achieving its objective. We consider window mean-payoff objectives: these are finitary versions of the traditional mean-payoff objective, obtained by replacing the long-run average of the payoffs by average payoffs computed over a finite sliding window. We present complexity bounds and algorithmic solutions for computing strategies of Player 1 to ensure that the objective is satisfied with positive probability, with probability 1, or with probability at least p, regardless of the strategy of Player 2. The solution crucially relies on a reduction to the special case of non-stochastic two-player games with the same objective. We also give a general characterisation of prefix-independent objectives for which this reduction holds. }, datum={12 April 2024 11:00}, note={Room 1Z14} } @talk{con24, author={Sylvain Conchon}, homepage={https://usr.lmf.cnrs.fr/~conchon/}, institution= {LMF}, title={Introduction à Cubicle, un vérificateur de modèles mettant en oeuvre le paradigme MCMT (Model Checking Modulo Theory)}, datum={15 March 2024 11:00}, note={Room 1Z18} } @talk{dem24, author={Stéphane Demri}, homepage={https://cv.hal.science/stephane-demri}, institution= {LMF}, title={Constraint Automata on Infinite Data Trees: from CTL(ℤ)/ CTL*(ℤ) to Decision Procedures}, datum={16 February 2024 11:00}, abstract={We introduce the class of tree constraint automata with data values in ℤ (equipped with the less than relation and equality predicates to constants), and we show that the nonemptiness problem is EXPTIME-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(ℤ) (CTL with constraints in ℤ) is EXPTIME-complete, and the satisfiability problem for CTL*(ℤ) is 2ExpTime-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed. This is a joint work with Karin Quaas (Leipzig University). Article available at <a href="https://drops.dagstuhl.de/opus/volltexte/2023/19023">drops.dagstuhl.de/.../19023</a>.}, note={Room 1Z76} } @talk{Demri24a, author={Stéphane Demri}, institution={LMF, CNRS}, homepage={https://cv.hal.science/stephane-demri}, title={First Steps Towards Taming Description Logics with Strings}, abstract={Paper: <a href="https://hal.science/hal-04212642">hal.science/hal-04212642</a>}, datum={26 January 2024 11:00}, note={Room 1Z71}, } @talk{bal24b, author={Benoît Ballenghien}, institution= {LMF}, title={Presentation of HOL-CSP: what, how and why? (2/2)}, datum={19 January 2024 11:00}, abstract={This will be a tutorial.}, note={Room 1Z56} } @talk{zha24, author={Kuize Zhang}, homepage={https://www.surrey.ac.uk/people/kuize-zhang}, institution= {University of Surrey, UK}, title={A new framework of discrete-event systems}, datum={17 January 2024 11:00}, abstract={The supervisory control theory (SCT) framework of discrete-event systems (DESs) initialized by Ramadge and Wonham (1934-2023) in the 1980s is one of four basic frameworks of DESs. Plenty of theoretical and applied results under this framework have been obtained. In this talk, I will present a new framework for DESs, under which the verification and enforcement of properties is based on a tool called concurrent composition. Compared with the SCT, the new framework has better scalability and wider implementability, hence the theoretical framework and applied areas of DESs will be largely extended. The new framework will be illustrated in verification and enforcement of strong detectability of labeled finite-state automata, which can be implemented in polynomial time. However, under SCT strong detectability enforcement cannot be implemented in polynomial time generally. In addition, I will present basic definitions on labeled weighted automata over monoids --- a new class of automata.}, note={Online} } @talk{ios24, author={Radu Iosif}, homepage={https://www-verimag.imag.fr/Radu-Iosif.html}, institution= {Verimag}, title={Proving Correctness of Self-Adapting Distributed Networks}, datum={15 January 2024 14:00}, abstract={We introduce a simple formal model to reason about the behaviors of self-adapting (reconfigurable) networks. The proofs of correctness of reconfiguration programs are done using a separation logic and a Hoare-style local reasoning proof system that produces proof obligations in the form of logical entailments. In particular, entailments are used to reason about invariance of assertions under interaction events (synchronous communication). In the second part of the talk, I will present some advances in deciding the validity of entailments in the dialect of separation logic used to model distributed networks. The decision procedure for the entailment problem relies on Courcelle’s Theorem stating the decidability of MSO for graphs of bounded tree-width and uses two novel techniques: 1. a computation of a bound on the tree-width of the models of a given separation logic formula (iff one exists) and 2. a push-button translation of (a significant fragment of) separation logic into MSO.}, note={Room 1Z76} } @talk{bal24a, author={Benoît Ballenghien}, institution= {LMF}, title={Presentation of HOL-CSP: what, how and why? (1/2)}, datum={12 January 2024 11:00}, abstract={This will be a tutorial.}, note={Room 1Z56} } % ======= 2023 ======= @talk{cle23, author={Émily Clément}, institution= {IRIF}, title={Higher Dimensional Timed Automata}, datum={15 December 2023 11:00}, abstract={Higher Dimensional Automata (HDA) are a very powerful tool to represent non-interleaving concurrency (i.e. a || b =/= a.b + b.a). They generalise numerous models, such as Petri nets. Languages of HDA are sets of ipomsets, which represent the possible order on the events. In recent years, interest in HDAs has increased and has lead to numerous new results (e.g 2021 Fahrenberg et al., 2023: Fahrenberg et al.). In our current work, we propose a new model, called Higher Dimensional Timed Automata, to obtain a more refined information on posets: rather than only the precedence order, we are interested in the time intervals in which events are active. In this model, we augment HDA with clocks and guards. Our goals are to define the language of HDTA, show that it generalises TA and study classical properties.}, note={Room 1Z61} } @talk{man23, author={Alessio Mansutti}, institution= {IMDEA Software Institute (Spain)}, title={Presburger Arithmetic with Divisibility Constraints: Applications and Algorithms}, datum={8 December 2023 14:00}, abstract={Presburger arithmetic, that is the first-order theory of the integers with addition and order, plays a pivotal role in various areas of computer science, encompassing both theoretical and practical applications. In the 70s, Leonard Lipshitz established a surprising result: while solving system of polynomial equations is an undecidable problem, adding to the existential fragment of Presburger arithmetic a divisibility predicate between linear polynomials results in a decidable theory. This theory, commonly referred to as EPAD (acronym for Existential Presburger Arithmetic with Divisibility), has recently found several applications to problems stemming from word equations and automata theory. Because of these applications, the exact complexity of the satisfiability problem for EPAD is nowadays considered a fundamental problem in arithmetic theories. It is known to lie in NEXPTIME, but no lower bound other than the straightforward NP-hardness from solving system of inequalities over the integers is known. In this talk, I will introduce EPAD and its aforementioned applications, and present the core ideas behind the original procedure by Lipshitz. I will then discuss recent improvements to this procedure, and explain the main obstacles to improving the current lower and upper bounds. This talk is in part based on the paper "Integer Programming with GCD Constraints" co-authored with Rémy Défossez, Christoph Haase and Guillermo A. Pérez (accepted for publication in SODA'24, pre-print available at <a href="https://arxiv.org/abs/2308.13609">arxiv.org/abs/2308.13609</a>).}, note={Room 1Z28} } @talk{Pascual23, author={Romain Pascual}, institution={MICS, CentraleSupélec, Université Paris-Saclay}, homepage={https://romainpascual.fr}, title={An approach for inferring geometric expressions in topology-based modeling}, abstract={Slides: <a href="https://romainpascual.fr/talk/fmai2023/FMAI2023_slides.pdf">romainpascual.fr/.../FMAI2023_slides.pdf</a>}, datum={6 October 2023 11:00}, note={Room 1Z56}, } @talk{Fervari23, author={Raul Fervari}, institution={Universidad Nacional de Córdoba / CONICET; Guangdong Technion - Israel Institute of Technology}, homepage={https://rfervari.github.io}, title={Updating Knowing How}, abstract={Slides: <a href="https://cs.famaf.unc.edu.ar/~rfervari/files/talks/2023-lmf.pdf">cs.famaf.unc.edu.ar/.../2023-lmf.pdf</a>}, datum={29 September 2023 11:00}, note={Room 1Z56}, } @talk{Topcu23, author={Ufuk Topcu}, institution={The University of Texas at Austin}, homepage={https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu}, title={Autonomous systems in the intersection of formal methods, learning, and control}, datum={23 June 2023 14:00}, note={Room 1Z18}, } @talk{dem23, author={Stéphane Demri}, homepage={https://cv.hal.science/stephane-demri}, institution= {LMF}, title={Model-Checking for Ability-Based Logics with Constrained Plans}, datum={9 June 2023 11:00}, abstract={We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of ``knowing how''. We consider several standard ability-based knowing how logic, for which we show that model-checking is PSPACE-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTIME model-checking problem. Furthermore, we extend with budgets the above-mentioned ability-logics, as done for ATL-like logics and energy games. We show that for the former logic enriched with budgets, the complexity increases to at least EXPSPACE-hardness. Other variant logics are discussed as well as a few open problems. This is joint work with Raul Fervari (University of Cordoba, Argentina) presented at AAAI’23. The paper is available at <a href="http://cv.hal.science/stephane-demri">cv.hal.science/stephane-demri</a>.}, note={Room 1Z71} } @talk{sou23, author={Thomas Soullard}, institution= {LMF}, title={Strategy synthesis with multiple observers}, datum={26 May 2023 14:00}, note={Room 1Z76} } @talk{Brucker23, author={Achim Brucker}, institution={Chair of Cybersecurity, University of Exeter, UK}, homepage={https://brucker.ch}, title={Towards the Formal Verification of Neural Networks in Isabelle/HOL}, datum={26 May 2023 11:00}, note={Room 1Z56}, } @talk{bor23, author={Benjamin Bordais}, institution= {LMF}, title={Playing (almost-)optimally in concurrent games with reachability and Büchi objectives }, datum={24 March 2023 11:00}, abstract={In a two-player win/lose concurrent graph game, two players at a given state concurrently (i.e., simultaneously) choose an action (among a finite set of available actions) which leads to another state. The process is repeated indefinitely thus forming an infinite sequence of states. The winner of the game is determined by an objective (i.e., a subset of infinite sequences of states). Concurrent games are more general than their turn-based counterparts in which, at each state, only one player chooses the next state to visit. However, this comes at the cost of not enjoying the desirable properties that turn-based games do. For instance, in turn-based games with parity objectives, there are always optimal strategies that are deterministic and positional whereas optimal strategies do not exist in general in concurrent games. In this talk, I will illustrate the turn-based and concurrent formalisms and show on specific examples why concurrent games behave more poorly than turn-based games. I will then briefly give the idea of how to build concurrent games that are more general than turn-based games but still enjoy similar properties that turn-based game do for the reachability objective.}, homepage={http://www.lsv.fr/~bordais/}, note={Room 1Z18} } @talk{mun23, author={Eric Munday}, institution= {U. of Edinburgh, Scotland}, title={Strategy complexity of lim sup in countable MDPs}, datum={21 March 2023 14:00}, abstract={In this talk we look at the strategy complexity of a lim sup objective in countable MDPs equipped with transition based rewards. This lim sup objective generalises the Buchi objective which is a well studied objective in verification. We will sketch three upper bound results, one epsilon-optimal and two different optimal upper bounds. We will take special care to highlight the techniques common to each proof which will hopefully convey the essence of what characterises lim sup.}, homepage={https://www.inf.ed.ac.uk/people/students/Eric_Munday.html}, note={Room 1Z56} } @talk{van23, author={Pierre Vandenhove}, institution= {LMF & Université de Mons}, title={How to Play Optimally for Regular Objectives?}, datum={17 February 2023 11:00}, abstract={We study two-player zero-sum games played on graphs and make contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of the first player is that eventually the sequence of colors along the play belongs to some regular language over finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets. These results are based on joint work with Patricia Bouyer, Nathanaël Fijalkow, and Mickael Randour and are available in the preprint at <a href="https://arxiv.org/pdf/2210.09703.pdf">arxiv.org/pdf/2210.09703.pdf</a>.}, homepage={http://math.umons.ac.be/staff/Vandenhove.Pierre/}, note={Room 1Z18} } % ======= 2022 ======= @talk{gov22, author={R. Govind}, homepage={https://rdnivog.github.io/}, institution= {Institute of Mathematical Sciences (IMSc), Chennai, India}, title={Simulations for Event-Clock Automata}, datum={31 October 2022}, note={Room tba}, } @talk{gastein22, author={Paul Gastin}, homepage={https://lsv.ens-paris-saclay.fr/~gastin/}, institution= {LMF, CNRS & ENS Paris-Saclay}, title={Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages}, datum={06 October 2022}, note={Room tba}, } @talk{boudec22, author={Patricia Bouyer-Decitre}, homepage={https://lmf.cnrs.fr/PatriciaBouyer/}, institution= {LMF}, title={Zone-based verification of timed automata: extrapolations, simulations and what next?}, datum={03 October 2022}, note={Room tba}, } @talk{ohlmann22, author={Pierre Ohlmann}, institution= {University of Warsaw}, title={Infinite duration games, memory, and graphs}, datum={10 October 2022 14:00 }, abstract={In this talk, I will give a broad overview of the field of infinite duration games: why do we care about them, and what are the main open questions. I will then discuss a new approach for making progress on these questions by reducing them to problems about (directed) graphs. The talk starts at 2pm.}, homepage={https://www.irif.fr/~ohlmann/}, note={Room 1Z69} } @talk{doyen22, author={Laurent Doyen}, institution= {LMF}, title={Stochastic Games with Synchronizing Objectives}, datum={27 June 2022 16:15 }, abstract={Revisiting a talk given at Etiolles 2022, in a "groupe-de-travail" style.}, homepage={http://www.lsv.fr/%7Edoyen/index.html}, note={Room 2U42} } @talk{guha22, author={Shibashis Guha}, institution= {Tata Institute of Fundamental Research, Mumbai}, title={PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP}, datum={24 June 2022 11:00 }, abstract={Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the fundamental models for non-deterministic systems with probabilistic uncertainty. Mean payoff (a.k.a. long-run average reward) is one of the most classic objectives considered in their context. We will discuss an algorithm to compute mean payoff probably approximately correctly in unknown MDP; further, we extend it to unknown CTMDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability, which has been advocated in literature. Joint work with Chaitanya Agarwal, Jan Křetínský and M. Pazhamalai }, homepage={https://www.tifr.res.in/~shibashis.guha/}, note={Room 1S69} } @talk{nowak22, author={Thomas Nowak}, institution= {LISN}, title={Reaching Consensus in Hostile Environments}, datum={15 April 2022 11:00 }, 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.}, homepage={https://www.thomasnowak.net}, note={Room 1Z28}, } @talk{civit22, author={Pierre Civit}, homepage={https://pcivit.github.io/}, institution= {LIP6}, title={Dynamic I/O Automata}, datum={21 January 2022 11:00 }, abstract={We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism from Attie & Lynch to probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. Our work extends to probabilistic settings all these features. Furthermore, we prove sufficient (weak) conditions to obtain the implementation monotonicity with respect to automata creation and destruction, i. e. if i) the automaton A supplants the automaton B in a new dynamic system X_A every time B appears in the old dynamic system X_B, and ii) A implements B, then the new dynamic system X_A implements the old dynamic system X_B.}, note={Room tba}, } % ======= 2021 ======= @talk{raine21, author={Raine Rönnholm}, institution= {University of Tampere, Finland}, title={How can we learn to coordinate?}, datum={21 May 2021 11:00}, abstract={Our general question is to study how (and when) rational players can coordinate their actions efficiently without any means of communication or conventions. We model games in a novel way as relational structures: in the case of pure win-lose coordination games they correspond to hypergraphs, which allows us to analyze them conveniently with graph theoretic methods. As an illustration of our approach, we identify optimal strategies for a fundamental class of repeated two player coordination games called "choice matching games".}, note={Room tba}, } @talk{23apr21, author={Pierre Vandenhove}, homepage={http://www.lsv.fr/~vandenhove/}, title={Arena-independent finite-memory strategies}, datum={23 April 2021 11:00}, note={Room tba}, } @talk{12mar21, datum={12 March 2021 11:00}, author={Aiswarya Cyriac}, institution= {CMI}, homepage={https://www.cmi.ac.in/~aiswarya/}, title={Weighted Tiling Systems for Graphs: Evaluation Complexity (part 2)}, abstract = {Follow-up on the talk of 19 Feb.}, note={Room tba}, } @talk{Rustam21, datum={5 March 2021 11:00}, author={Rustam Galimullin}, homepage={https://rgalimullin.gitlab.io/}, institution= {University of Bergen}, title = {Group Knowledge in Public Communication}, note={Room tba}, } @talk{19feb21, datum={19 Februar 2021 11:00}, author={Aiswarya Cyriac}, institution= {CMI}, homepage={https://www.cmi.ac.in/~aiswarya/}, title={Weighted Tiling Systems for Graphs: Evaluation Complexity (part 1)}, note={Room tba}, } @talk{kickoff, datum={29 Jan 2021 11:00}, title={Kick-off meeting}, note={Room tba}, } @talk{SergeJan21, datum={2021-01-22}, author={Serge Haddad}, homepage={https://home.lmf.cnrs.fr/SergeHaddad/}, institution= {LMF}, title={Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models}, note={Room tba}, }

Contact

LMF - Laboratoire Méthodes Formelles
Université Paris-Saclay, CNRS, ENS Paris-Saclay
4 avenue des Sciences
91190 Gif-sur-Yvette, France

Phone: +33 (0)1 81 87 54 50

Mail : contact@lmf.cnrs.fr