• Login

en fr

GT Informel Seminar series of the teams Distributed Computing and Model-Checking & Synthesis

Format

The seminar inFormel welcomes presentations from the members of the groups Concurrency & Distributed Systems and Model-checking & Synthesis about ongoing work or interesting reading related to the area of the two groups. The seminar may occasionally host speakers visiting LMF.

Where and when

Currently seminars are held in a hybrid mode on

Fridays, 11h00.

Please mind that the room and viso link may change per talk. Check the talk's description for the room. Visio links are distributed internally. Let us know if you are interested in attending a talk - we are happy to send you the link.

@next{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}, institution= {MPI Saarbrücken}, 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}, 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 [[http://gossner.me/wp-content/uploads/2023/01/rationalizable.pdf]]} } @talk{guh24b, author={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}, 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{gab24, author={Pranshu Gaba}, 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}, 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}, 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 [[https://drops.dagstuhl.de/opus/volltexte/2023/19023 | https://drops.dagstuhl.de/opus/volltexte/2023/19023]].}, note={Room 1Z76} } @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}, 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}, 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} } @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 [[https://arxiv.org/abs/2308.13609 | https://arxiv.org/abs/2308.13609]]).}, note={pm Room 1Z28} } @talk{dem23, author={Stéphane 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 [[http://cv.hal.science/stephane-demri | http://cv.hal.science/stephane-demri]].}, note={1Z71} } @talk{sou23, author={Thomas Soullard}, institution= {LMF}, title={Strategy synthesis with multiple observers}, datum={26 May 2023 14:00}, note={pm Room 1Z76} } @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={pm 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 [[https://arxiv.org/pdf/2210.09703.pdf | https://arxiv.org/pdf/2210.09703.pdf]].}, homepage={http://math.umons.ac.be/staff/Vandenhove.Pierre/}, note={Room 1Z18} } @talk{gov22, author={R. Govind}, title={Simulations for Event-Clock Automata}, datum={31 October 2022} } @talk{gastein22, author={Paul Gastin}, title={Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages}, datum={06 October 2022} } @talk{boudec22, author={Patricia Bouyer-Decitre}, title={Zone-based verification of timed automata: extrapolations, simulations and what next?}, datum={03 October 2022} } @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={pm 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}, 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.} } @talk{raine21, author={Raine Rönnholm}, 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".} } @talk{23apr21, author={Pierre Vandenhove}, homepage={http://www.lsv.fr/~vandenhove/}, title={Arena-independent finite-memory strategies}, datum={23 April 2021 11:00} } @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.} } @talk{Rustam21, datum={5 March 2021 11:00}, author={Rustam Galimullin}, title = {Group Knowledge in Public Communication} } @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)}, } @talk{kickoff, datum={29 Jan 2021 11:00}, title={Kick-off meeting}, } @talk{SergeJan21, datum={2021-01-22}, author={Serge Haddad}, title={Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models} }

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