Logo IRISA logo Inria

Prochain Exposé

jeudi 22 fevrier, 14h en salle Minquiers

Serge Haddad

Réseaux de Petri discrets et continus : apports réciproques

Dans les années 80, les réseaux de Petri continus (RdPC) ont été introduits d'une part pour remédier à l'explosion combinatoire des réseaux de Petri discrets (RdP) et d'autre part pour modéliser le comportement de systèmes physiques dont l'état est spécifié par des variables continues. Depuis cette époque, différents travaux ont établi que la complexité de la vérification de propriétés comportementales se réduit en passant du modèle discret au modèle continu. Cet exposé consistera en trois parties. Tout d'abord je détaillerai un algorithme polynomial pour l'accessibilité dans les RdPC et survolerai les autres algorithmes polynomiaux pour RdPC. Je montrerai aussi que l'accessibilité est PTIME-complète tandis que l'absence de blocage est coNP-complète. J'étudierai ensuite l'application de ces procédures au problème de couverture des RdP. La couverture est particulièrement appropriée à l'étude de programmes concurrents à mémoire partagée. Cependant sa complexité élevée (EXPSPACE-complète) limite son utilisation pour des problèmes de taille industrielle. Aussi je développerai une nouvelle approche appliquant la couverture des RdPC comme méthode d'élagage d'un algorithme de couverture en arrière. Le point crucial est ici un codage efficace de l'algorithme polynomial en une formule d'un SMT solveur. Finalement je montrerai que ce codage peut aussi être appliqué au problème d'inclusion d'ensembles d'accessibilité de RdPC réduisant ainsi la complexité de EXPTIME à coNP. J'établirai aussi que cette procédure est optimale, i.e. le problème est coNP-complet.

Exposés des semaines suivantes

jeudi 15 mars, 14h en salle Lipari

Blaise Genest

TBA

TBA

jeudi 22 mars, 14h en salle Aurigny

Sophie Pinchinat

The ATSyRA tool: an environment for the assisted design and analysis of Attack Trees

I will present the formal setting we develop to support the functionalities of the tool ATSyRA (some of them are under development). In a nutshell, the tool allows experts to:
- specify a system (currently a building);
- specify an attack goal, and more generally an attack tree;
- verify properties of a tree w.r.t. the system;
- ask for many kinds of witnesses regarding attacks.
This project is supported by DGA Bruz. It involves members of IRISA from several teams, Yann Thierry-Mieg from LIP6 and the end-user Lionel van Aertryck from DGA Bruz.

jeudi 29 mars, 14h en salle Minquiers

Philippe Schnoebelen (CNRS & ENS Paris-Saclay)

Decidable fragments of the logic of subwords

While subwords appear prominently in many works in language theory, program verification, combinatorics on words, etc., not much is known about the decidability of logics for subwords and subsequences.
In this talk we present several recently identified fragments of the first-order logic of subwords that have been shown decidable. We also describe some new techniques from the descriptive complexity of piecewise-testable languages that have been used in the complexity analysis of our decidable logic fragments.

Séminaire autour des thèmes 68NQRT