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.

Date | Orateur | Titre | Hybride / Virtuel |
---|---|---|---|

mardi 20 septembre | Christoph Haase (University of Oxford) | Directed Reachability for Infinite-State Systems | Hybride |

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 octobre | Laurent Doyen (LMF, ENS Paris-Saclay) | Stochastic Games with Synchronizing Objectives | Virtuel |

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 octobre | Pierre Ohlmann | Infinite duration games, memory, and graphs | Hybride |

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 novembre | Mikołaj Bojanczyk | TBA | Virtuel |

TBA | |||

mardi 22 novembre | Nathalie Bertrand | TBA | TBA |

TBA |

- Méthodes Formelles 2016-....
- Graphes et Logique 2010-2015.
- Modélisation et Vérification 2010-2015.
- MVTsi 2009-2010.
- MVTsi 2008-2009.
- MVTsi 2007-2008.
- MVTsi 2006-2007.
- MVTsi 2005-2006.
- MVTsi 2004-2005.
- MVTsi 2003-2004.
- MVTsi 2002-2003.
- MVTsi 2001-2002.
- MVTsi 2000-2001.
- MVTsi 1999-2000.
- MVTsi 1998-1999.
- MVTsi 1997-1998.
- MVTsi 1996-1997.
- MVTsi 1995-1996.
- Sémantique du parallélisme 1994-1995.
- Sémantique du parallélisme 1993-1994.
- Sémantique du parallélisme 1992-1993.