Séminaire de l'équipe Méthodes et Modèles Formelles (M2F)

LaBRI, Bordeaux

Le séminaire M2F a lieu salle 178 un mardi sur deux à 14H.

Pour proposer un séminaire, le calendrier vous aidera à choisir une date disponible.

Pour s'abonner ou se désabonner de la liste de diffusion.

Pour s'inscrire au calendrier de l'équipe M2F.


Prochains exposés

DateOrateurTitreHybride / Virtuel
mardi 20 septembreChristoph Haase (University of Oxford)Directed Reachability for Infinite-State SystemsHybride
Directed model checking is a bug-finding technique that emerged in the late 1990s, primarily applied to finite-state systems and infinite-state systems with finite quotient graphs such as timed automata. Recent progress in the areas of optimisation modulo theories and arithmetic abstractions of infinite-state systems makes it possible to apply this technique to efficiently (semi-)deciding reachability in inherently infinite-state systems that may even have undecidable reachability problems. In this talk, I will give an introduction to the ideas underlying directed model checking and demonstrate how it can be used to semi-decide reachability problems in large-scale Petri nets. This talk is based on joint work with M. Blondin and Ph. Offtermatt (Sherbrooke, CA)
mardi 4 octobreLaurent Doyen (LMF, ENS Paris-Saclay)Stochastic Games with Synchronizing ObjectivesVirtuel
We consider two-player stochastic games played on a finite graph for infinitely many rounds. Stochastic games generalize both Markov decision processes (MDP) by adding an adversary player, and two-player deterministic games by adding stochasticity. The outcome of the game is a sequence of distributions over the states of the game graph. We consider synchronizing objectives, which require the probability mass to accumulate in a set of target states, either always, once, infinitely often, or always after some point in the outcome sequence; and the winning modes of sure winning (if the accumulated probability is equal to 1) and almost-sure winning (if the accumulated probability is arbitrarily close to 1). We present algorithms to compute the set of winning distributions for each of these synchronizing modes, showing that the corresponding decision problem is PSPACE-complete for synchronizing once and infinitely often, and PTIME-complete for synchronizing always and always after some point. These bounds are remarkably in line with the special case of MDPs, while the algorithmic solution and proof technique are considerably more involved, even for deterministic games. This is because those games have a flavour of imperfect information, in particular they are not determined and randomized strategies need to be considered, even if there is no stochastic transitions in the game graph. Moreover, in combination with stochasticity in the game graph, finite-memory strategies are not sufficient in general (for synchronizing infinitely often).
mardi 18 octobrePierre OhlmannInfinite duration games, memory, and graphsHybride
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 to making progress on these questions by reducing them to problems about (directed) graphs.
mardi 8 novembreMikołaj BojanczykTBAVirtuel
TBA
mardi 22 novembreNathalie BertrandTBATBA
TBA



Calendrier de l'équipe




Archives des années précédentes

Exposés passés depuis 2017.




Responsables

Igor Walukiewicz, Corto Mascle