Site menu:



Quatre orateurs invités à MSR2017


Claudine CHAOUIYA - Site web
Instituto Gulbenkian de Ciência, Portugal

Titre de l'exposé : Prolifération, différenciation, mort cellulaire… Comprendre le destin des cellules en modélisant leurs réseaux moléculaires

Résumé de l'exposé ... Résumé de l'exposé


Les processus cellulaires majeurs sont contrôlés par des réseaux d'interactions complexes et hétérogènes, et les dysfonctionnements de ces réseaux sont associés à de nombreuses maladies. Après un bref panorama des approches de modélisation considérées pour aborder ces réseaux, je présenterai le formalisme logique de René Thomas. L'analyse des dynamiques discrètes de ces modèles logiques est particulièrement difficile et pourrait bénéficier des techniques développées par la communauté des automaticiens et informaticiens. Pour illustrer ces défis, je présenterai les travaux de mon équipe sur des méthodes d'analyse qui seront appliquées sur un modèle de la régulation des propriétés adhésives des cellules cancéreuses.


Biographie de l'orateur ... Biographie de l'orateur


Claudine Chaouiya a obtenu un Doctorat en Informatique en 1992 à Nice Sophia Antipolis. Après avoir occupé un poste de professeur invité au Brésil puis de Maitre de Conférences en Nouvelle Calédonie, elle a rejoint l'Université d'Aix-Marseille en 1999. C'est à Marseille qu'elle a commencé à s' intéresser aux réseaux biologiques, avec l'idée que ses connaissances de modélisation et analyse de systèmes industriels trouveraient là un champ d' application passionnant. Depuis 2008, elle est en détachement au Portugal, à l'Institut Gulbenkian de Science, où elle dirige sa propre équipe de recherche. Ses travaux sont menés en collaboration étroite avec des biologistes et sont organisés selon deux axes majeurs: la modélisation de processus biologiques et les développements méthodologiques pour une analyse efficaces de ces modèles.


Serge HADDAD - Site web
LSV, ENS Cachan, France

Titre de l'exposé : Réseaux de Petri discrets et continus : apports réciproques

Résumé de l'exposé ... Résumé de l'exposé


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.


Biographie de l'orateur ... Biographie de l'orateur


Serge Haddad est un ancien élève de l'ENS Cachan en mathématiques. Son doctorat (soutenu en 1987) était consacré à l'analyse des réseaux de Petri de haut-niveau. Depuis il a été successivement maître de conférences de 1988 à 1993 à l'Université Pierre et Marie Curie, puis professeur à l'Université Paris-Dauphine et depuis 2008 à l'ENS Cachan. Ses travaux (qui lui ont valu 5 récompenses en conférence internationale) portent sur la vérification et le contrôle de systèmes à événements discrets présentant des aspects quantitatifs tels que le temps et les probabilités.



Stéphane LAFORTUNE - Site web
Université du Michigan, Ann Arbor, États-Unis

Titre de l'exposé : Contrôle par supervision des systèmes à événements discrets : Rétrospective et Perspectives

Résumé de l'exposé ... Résumé de l'exposé


L’année 2017 marque le trentième anniversaire de la publication dans la littérature en automatique des articles de Ramadge et Wonham qui ont introduit la théorie du contrôle par supervision des systèmes à événements discrets modélisés dans le cadre des langages formels et des automates finis. Cette théorie a par la suite été étendue à plusieurs catégories d'architectures de contrôle avec modularité horizontale ou verticale. En parallèle, le domaine des méthodes formelles en informatique a fait des progrès considérables en vérification des systèmes fermés ainsi qu'en synthèse des systèmes réactifs. Récemment, le domaine des méthodes formelles en automatique a pris de l'ampleur, en particulier dans le cadre des systèmes cyber-physiques qui sont abstraits en systèmes discrets soumis à des spécifications en logique temporelle. Nous allons discuter comment ces domaines de recherche sont complémentaires. Nous allons aussi présenter des résultats récents sur la synthèse de contrôleurs et de stratégies d'activation des capteurs pour les systèmes discrets à observation partielle d'événements. Nous allons conclure la présentation avec des perspectives sur les algorithmes pour la synthèse des contrôleurs qui exploitent les méthodes symboliques et les résultats récents dans la technologie des solveurs du problème SAT.


Biographie de l'orateur ... Biographie de l'orateur


Stéphane Lafortune est Professeur au département “Electrical Engineering and Computer Science” à l’université du Michigan, Ann Arbor, EU. Il a obtenu ses diplômes en génie électrique de l’Ecole Polytechnique de Montréal (B.Ing, 1980), l’université McGill (M.Eng, 1982), et l’université de California à Berkeley (PhD, 1986). Lafortune est un “Fellow” de l’IEEE (1999) et de l’IFAC (2017). Ses recherches couvrent tous les aspects des systèmes à événements discrets, incluant la modélisation, le contrôle, le diagnostic et l’optimisation, avec applications aux systèmes d’ordinateurs. Il est co-auteur, avec Christos Cassandras, du livre Introduction to Discrete Event Systems (2e édition, Springer, 2008). Il est Editeur-en-Chef du journal Discrete Event Dynamic Systems: Theory and Applications (Springer).



Joseph SIFAKIS - Site web
RSD Team, Verimag, France

Titre de l'exposé : Modeling architectures and their properties in BIP

Résumé de l'exposé ... Résumé de l'exposé


Architectures are mechanisms for ensuring global properties characterizing the coordination between components. Using architectures largely accounts for our ability to master complexity and develop systems cost-effectively. In BIP, architectures are generic behavior transformers represented as sets of connectors. They take as arguments typed components and give a composite component. We propose two different ways to describe architectures using respectively imperative and declarative languages. The imperative language, Dynamic BIP uses iterators on component variables and set-of-component variables to describe dynamic architectures. The declarative language is a second order Interaction Logic based on a symbolic representation of connectors. In BIP, architecture properties are architecture styles or patterns that characterize families of architectures sharing common characteristics such as Token-ring and Philter styles. Configuration Logic is a power-set extension of Interaction Logic used to specify architecture styles. We provide theoretical foundations of the above formalisms developed at EPFL and Verimag. We also provide examples illustrating their effective application. We conclude with a discussion on ongoing and future work directions aiming at the implementation and integration of these results in correct-by-construction system design flows.


Biographie de l'orateur ... Biographie de l'orateur


Joseph Sifakis is Emeritus Senior CNRS Researcher at Verimag. His current research interests cover fundamental and applied aspects of embedded systems design. The main focus of his work is on the formalization of system design as a process leading from given requirements to trustworthy, optimized and correct-by-construction implementations. Joseph Sifakis has been a full professor at Ecole Polytechnique Fédérale de Lausanne (EPFL) for the period 2011-2016. He is the founder of the Verimag laboratory in Grenoble, which he directed for 13 years. Verimag is a leading research laboratory in the area of embedded systems, internationally known for the development of the Lustre synchronous language used by the SCADE tool for the design of safety-critical avionics and space applications. In 2007, Joseph Sifakis has received the Turing Award for his contribution to the theory and application of model checking, the most widely used system verification technique today. Joseph Sifakis has had numerous administrative and managerial responsibilities both at French and European level. He has actively worked to reinvigorate European research in embedded systems as the scientific coordinator of the « ARTIST » European Networks of Excellence, for ten years. He has participated in many major industrial projects led by companies such as Airbus, EADS, France Telecom, Astrium, and STMicroelectronics. Joseph Sifakis is a member of the French Academy of Sciences, a member of the French National Academy of Engineering, a member of Academia Europea, a member of the American Academy of Arts and Sciences, and a member of the National Academy of Engineering. He is a Grand Officer of the French National Order of Merit, a Commander of the French Legion of Honor. He has received the Leonardo da Vinci Medal in 2012. Joseph Sifakis has received in 2009 the Award of the Hellenic Parliament Foundation for Parliamentarism and Democracy. He is a commander of the Greek Order of the Phoenix. He has been the President of the Greek Council for Research and Technology for the period February 2014 – April 2016.