Séminaires
Séminaire du 06 Octobre 2006
Lieu
Université Paris-Dauphine: comment y aller
Programme
14h00-15h00: "La supervision des systèmes répartis, fondée sur le dépliage de modèles de réseaux de Petri symboliques et temporisés" par Claude Jard, Professeur ENS Cachan
Abstract: un objectif de la supervision en univers réparti est de retrouver les dépendances causales entre les événements observés du système. Lorsque l'information observée est partielle, nous avons recours à un modèle pour pouvoir les inférer. Nous proposons d'utiliser les réseaux de Petri, y compris dans leurs extensions symboliques (réseaux colorés) et temporisées (réseaux temporels). La technique algorithmique repose sur la construction de dépliages, guidée par les observations. L'exposé présentera le problème, les modèles, les techniques et des exemples d'application.
15h00-15h30 : "Emptiness Check of Powerset Büchi Automata using Inclusion Tests : Application to Well Formed Nets" par Souheib Baarir doctorant au LIP6 (travail joint avec Alexandre Duret-Lutz)
Abstract: he automata-theoretic approach to model-checking uses automata on infinite words to represent a system as well as a property to check on it. Both automata are synchronized, and the resulting product automaton is examined by an emptiness check. One drawback of this approach, known as the state explosion problem, lies in the large size of the automaton used to represent the behavior of the system, and hence in the resulting size of the product automaton that has to be explored by the emptiness check. If the state space has a global symmetry (for example a client/server system where all clients behave identically), it is easy to ``fold'' the automaton by factorizing the representations of its symmetric states. However such globally symmetric automata are uncommon in practice. This work introduces two emptiness checks for ''partially symmetric systems'': usually the state space is constructed on-the-fly during the emptiness check, and we show that during this emptiness check it is possible to perform ''inclusion tests'' to limit the number of constructed states, further reducing the complexity of the verification, for ''partially symmetric systems''. Because this idea can be useful in general (i.e., not only to symmetries), we present our new emptiness check in a general framework of ''powerset automata".