L'essor d'Internet et des nouvelles technologies fait que l'informatique est au centre des moyens de communication actuels. Ces avancées technologiques impliquent un changement considérable de nos modes de consommation et de communication. Tous ces échanges de messages sont gérés par des protocoles de communications complexes que l'utilisateur ne contrôle pas totalement. Les usagers souhaitent que leurs communications soient "sécurisées". Les concepteurs de ces protocoles de communication sécurisent grâce à des méthodes cryptographiques les échanges de messages dans un environnement "hostile". Un tel environnement est constitué d'un participant malhonnête appelé intrus ou attaquant. Nous supposons que l'intrus contrôle le réseau sur lequel les messages sont échangés. La vérification des protocoles cryptographiques assure qu'il n'existe pas d'attaque possible lors d'une exécution du protocole face à un certain intrus. Une des hypothéses importantes faites en vérification de protocoles cryptographiques est "l'hypothése de chiffrement parfait" : le seul moyen d'obtenir le contenu d'un message chiffré est de connaître la clef de déchiffrement. Si un protocole est prouvé sûr sous cette hypothése de chiffrement parfait, cela est insuffisant pour assurer qu'une information confidentielle échangée sur le réseau grâce à un protocole cryptographique entre deux participants reste secrète. Il se peut que certaines propriétés algébriques utilisées dans le protocole permettent à l'intrus d'obtenir de l'information. Un des moyens pour affaiblir l'hypothèse de chiffrement parfait, et donc d'analyser de manière plus réaliste les protocoles, est de prendre en compte certaines propriétés algébriques dans le modèle de vérification. Je présenterai dans cet exposé, une approche formelle pour la vérification de la propriété de secret d'information pour les protocoles cryptographiques en présence d'une théorie équationnelle : la théorie du "ou exclusif" et de l'homomorphisme.

Testing may be used to show that a system under test conforms to its specification. In the case of a distributed system, one may have to use a distributed test architecture, involving $p$ testers in order to test the system under test. These $p$ testers may under some circumstances have to coordinate their actions with each other using external coordination channels. This may require the use of up to $p2-p$ unidirectional coordination channels in the test architecture, which can be an extensive and expensive setup.
In this presentation, we will review an existing method for generating checking sequences for testing multi ports machines; we will adapt this method to generate checking sequences while attempting to minimize the number of required coordination channels.

On s'intéresse aux relations rationnelles qui sont les relations réalisées par des automates à plusieurs bandes. On considère les quatre familles des relations reconnaissables, synchrones, déterministes et rationnelles. Elles forment une hiérarchie stricte et on étudie le problème de décision suivant. Étant donnée une relation, appartient-elle à une famille plus petite. On rappelle les résultats déjà connus et on montre quelques résultats nouveaux.

Dans cet exposé on considérera la famille des arbres rationnels, c'est-à-dire des graphes rationnels qui sont des arbres. On examinera, dans un premier temps un certain nombre d'exemples, et de résultats élémentaires. Ensuite, on observera la décidabilité de logiques dans cette famille à l'aide d'exemples. Pour finir, on démontrera la décidabilité de la logique du premier ordre pour les arbres rationnels.

Les auteurs de [AVW03] étudie la décidabilité de la synthèse de contrôleurs lorsque les spécifications sont exprimées par le mu-calcul modal. Ils utilisent une extension de cette logique pour spécifier que certains événements auxquels réagit le système sont inobservables pour le contrôleur. Cette approche permet de spécifier les problèmes classiques de la théorie du contrôle des systèmes a événements discret avec observation partielle.
Cet expose rappellera les principaux résultats de [AVW03] et présentera une extension du mu-calcul modal permettant de définir des contraintes d'indiscernabilité. Il s'agit de spécifier que le contrôleur peut détecter un signal mais ne peut discerner a quel événement il correspond: certains événements sont indiscernables pour le contrôleur. Certains résultats sur la décidabilité du contrôle centralise et décentralise, avec des contraintes d'indiscernabilité et d'inobservabilite, seront présentées.
Cet expose présentera aussi une extension de la notion d'information partielle. Nous considérons le cas ou le contrôleur ne peut distinguer, non pas des événements, mais des comportements du SED.
[AVW03]A. Arnold, A. Vincent and I. Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science vol. 303(1) (2003) pp. 7-34.

En 2003, A.Arnold, A.Vincent et I.Walukiewicz ont propopsé une méthode pour synthétiser des contrôleurs spécifiés par des formules du mu-calcul.
Cette méthode a été partiellement implémentée dans l'outil Synthesis développé au LaBRI.
Cet exposé fera un bref rappel sur les algorithmes mis en oeuvre dans l'outil.
Ce rappel sera suivi d'une démonstration sur deux exemples de synthèse de contrôleurs.

Dans cet exposé on étend la logique propositionnelle dynamique (PDL) de Fischer et Ladner à l'aide d'une classe restreinte de programmes récursifs basés sur le formalisme des automates à pile à visibilité (Alur et Madhusudan 2004). On montre que le problème de la satisfaisabilité pour cette extension reste décidable et que cette approche généralise des résultats connus pour des extensions de PDL par des programmes infinis.

Ces travaux ont été effectués en collaboration avec Christof Löding (Aachen).

In this talk we present a methodology to construct distributed implementations from global specifications. The ingredients of the problem are: (a) the models of synchronous products of transition systems, respectively Zielonka's asynchronous automata as distributed implementations and (b) graph-isomorphism, trace-equivalence, respectively bisimilarity as correctness criteria of the distributed implementation w.r.t. the global specification.

`La carte du jour' of the presentation will consist of: (a) some preliminaries and characterizations regarding the distributed systems as appetizers, (b) checking the consistency of the global specification and heuristics for obtaining smaller distributed implementations as main courses, and (c) a case study (mutual exclusion) as dessert.

La technique du mode-checking regulier a été introduite dans les années 90 afin de modéliser des systèmes paramétrés. Chaque état du système est représenté par un langage régulier et les actions possibles par une relation R. Si l'on note I le langage regulier codant l'état initial, l'objectif devient alors de calculer R*(I) afin de connaître tous les états accessibles. Dans le cadre général, il est impossible de calculer R*(I) ; de nombreux travaux visent alors soit à fournir des techniques de calcul semi-algorithmiques, soit à restreindre R et I à des cas décidables. C'est dans ce dernier cadre que ce situe notre travail. Nous étendons un résultat de Bouajjani, Musholml et Touili (LICS01) à une classe de langages plus grande tout en améliorant l'efficacité du calcul de R*, lorsque R est une relation de semi-commutation.

Travail en commun avec Gérard Cécé et Yann Mainier

La théorie des jeux s'applique aux situations où plusieurs agents interagissent, et chacun défend son intérêt propre. Cette théorie trouve des applications dans plusieurs domaines, comme l'économie, la biologie et l'informatique. Ainsi, le concept de jeu est utilisé en théorie des ensembles (hiérarchie de Wadge), en logique (jeux d'Ehrenfeucht-Frayssé), dans la théorie des automates (complémentation des automates d'arbres infinis), ou encore en vérification (mu-calcul).

Dans cet exposé, on s'intéressera principalement au cas des jeux stochastiques à deux joueurs, à somme nulle, à information totale et à durée infinie. Une partie consiste en une infinité de tours de jeux. A chaque tour, le jeu est dans un certain état, et un des joueurs (Min et Max) choisit une action. Cette action détermine l'état suivant du jeu selon une certaine distribution de probabilités. Après une partie, la suite des états par lequel le jeu est passé détermine un paiement que le joueur Min doit verser au joueur Max. Le but du joueur Min est de minimiser la somme qu'il doit verser au joueur Max, alors que le joueur Max essaye de la maximiser. Pour y parvenir, les deux joueurs doivent employer des stratégies optimales.

Pour certaines fonctions de paiement, il est possible de calculer ces stratégies optimales, en particulier quand on est assuré de l'existence de stratégies optimales dites sans mémoire: le choix d'une action par un joueur ne dépend que de l'état courant du jeu, et pas de l'histoire entière de la partie. Dans ce cas, on dit que le jeu est positionnel.

Cela mène naturellement à la question de déterminer quels jeux sont positionnels. On présentera divers résultats liés à cette question, depuis l'article séminal de Shapley en 1953, jusqu'au nombreux travaux récents sur la question.

Dans une industrie du logiciel où la complexité des applications ne cesse de croître, un des objectifs du génie logiciel est de conserver l'intelligibilité du processus de construction et de maintenance de ces applications.

Dans ce cadre, le concept de composant a été introduit comme une extension du concept d'objet pour faciliter la conception d'applications réparties complexes, c'est-à-dire formées de nombreux éléments en coopération, distribuées sur différents sites d'exploitation, et contraints par des exigences variées (persistance, sécurité, tolérance aux pannes, etc.). Il existe à ce jour de nombreux modèles de composants avec des objectifs différents.

Cependant, un des points communs de ces modèles est la mise en lumière de l'architecture de l'application, c'est-à-dire une description de haut niveau de cette application décomposée en différents composants interconnectés et définis par leurs fonctionnalités requises et offertes. De par la complexité de certaines applications, la définition de l'architecture est elle-même une opération délicate. Entres autres, il est difficile de construire un assemblage de composants qui adresse l'ensemble des préoccupations d'une application en une seule étape. L'objectif de ces travaux est alors de proposer une démarche de construction incrémentale où l'architecte peut à chaque étape ajouter une nouvelle préoccupation à son architecture. Malheureusement, les modèles de composants ne proposent en générale qu'une unique dimension de structuration d'une application. Dès lors, certaines préoccupations comme la sécurité, la persistance ou la tracabilité ne peuvent être correctement structurées au sein d'un seul composant et se retrouvent alors noyées au sein de nombreux éléments de l'architecture. Cette mauvaise structuration est très préjudiciable pour l'intégration de ces préoccupations dans une architecture existante. Nous proposons donc, dans une deuxième partie de cette thèse, un canevas de conception d'architecture nommé TranSAT qui permet l'intégration de nouvelles préoccupations dans une architecture par transformation de cette dernière. Ce canevas introduit la notion de patron d'architecture pour structurer les différentes préoccupations transverses d'une application. Ce patron comprend les éléments d'architecture à intégrer, les transformations à apporter sur l'architecture de base, mais aussi un ensemble de contraintes génériques sur les éléments d'une architecture cible sur laquelle le patron peut être intégré. De plus, TranSAT propose un langage dédié pour spécifier les modifications à apporter sur l'architecture de base afin d'intégrer la nouvelle préoccupation.

Les primitives de transformation de ce langage sont inspirées par les différentes sémantiques possibles de l'interaction entre un aspect et une classe de base en programmation par aspects. La spécialisation de ce langage permet de produire différentes analyses statiques afin de garantir la cohérence de l'architecture résultante sans analyser la totalité de cette architecture.

En perspective de ce travail, je montrerai dans quelle mesure une partie de ces travaux se généralisent dans le contexte de l'ingénierie dirigée par les modèles. Je proposerai ainsi une ébauche d'architecture pour la mise en place de la notion de patrons de modèles permettant de définir des opérateurs de transformation de haut niveau plus facilement réutilisables et propices à la construction incrémentale de modèles.

Voir aussi ici et:
Safe Integration of New Concerns in a Software Architecture. Olivier Barais, Julia Lawall, Anne-Fran?oise Le Meur and Laurence Duchien. In Proceedings of the 13th Annual IEEE International Conference on Engineering of Computer Based Systems (ECBS'06), Potsdam, Germany, March 2006, p 52 -- 61, ISBN 0-7695-2546-6

Je présenterais différentes techniques d'analyses de programmes en vu d'obtenir des bornes sur leur complexité. Ceci permet d'obtenir plusieurs caractérisations syntaxiques de classes de complexité usuelles comme Ptime ou Pspace. De plus, je mettrais l'accent sur les aspects de complexité implicite (complexité du programme comparée à la complexité de la fonction comparée) et d'intentionnalité (capturer le plus possible d'algorithmes "naturels" dans la caractérisation).

On considère un modèle probabiliste de système concurrent où les exécutions du système sont regardées uniquement du point de vue des ordres partiels qu'elles engendrent. On s'intéresse aux propriétés de synchronisation des systèmes dans ce contexte.

L'introduction des probabilités apporte les outils d'intégration qui permettent une étude fine de quantités a priori non bornées. Un temps particulièrement important dans l'étude des systèmes distribués est le temps de synchronisation entre composantes parallèles. Considérer un temps fini en moyenne (c-à-d, intégrable) permet de conserver des méthodes d'approche pour son étude sans éliminer trop de cas réalistes. On montre une application à une loi des grands nombres pour les réseaux de Petri markoviens, ce qui permet de définir le taux d'entropie moyen d'un tel réseau.

Vendredi 24 mars 2006 à 14h00 en salle Les Minquiers

Les systèmes auto-stabilisants sont des systèmes répartis naturellement tolérants aux défaillances. Un système auto-stabilisant est un système qui, quelque soit son initialisation et donc après une défaillance, finit par se comporter correctement. Un inconvénient souvent cité de l'auto-stabilisation est que la stabilisation ne peut être détectée par le protocole lui-même. En effet, si la détection se fait par un prédicat sur un ensemble de variables, la corruption de ces variables peut donner une fausse indication. Par contre, rien n'empêche un observateur extérieur de procéder à cette détection. Dans un article de PODC 98, Lin et Simon proposent un observateur réparti et montrent à l'aide d'exemples que la détection peut être plus courte que la stabilisation. L'observateur réparti utilise, en chaque site, une mémoire supposée incorruptible. Cette hypothèse, si elle est valide pour des réseaux locaux de petite taille, ne passe absolument pas à l'échelle.

Nous proposons un nouveau modèle, fondé sur des observateurs locaux, utilisant beaucoup moins de ressources. En particulier, un tel observateur est placé sur un seul site du système et permet de conclure, sous certaines conditions, à la stabilisation. Dans ce modèle, nous prouvons qu'il est possible de construire un observateur déterministe pour n'importe quelle tâche spécifiée sous un démon synchrone et pour une topologie distinguée, dès lors que cette tâche admet une solution auto-stabilisante. Nous introduisons également la notion d'observateur probabiliste et nous prouvons que de tels observateurs permettent d'observer une plus grande classe de systèmes auto-stabilisants que les observateurs déterministes.

We analyse the notion of iterated admissibility, i.e., avoidance of weakly dominated strategies, as a solution concept for infinite path-forming games. This concept is known to provide a valuable criterion for selecting among multiple equilibria and to yield sharp predictions in games with finitely many strategies. However, generalisations to infinite strategy spaces are typically problematic, due to unbounded dominance chains and the requirement of transfinite induction.

In a multi-player non-zero sum setting, we show that for path-forming games with only two possible outcomes (win or lose), the concept of iterated admissibility is sound and robust: all rationality stages are dominated by admissible strategies, the iteration terminates on finite graphs and, under regular winning conditions, strategies that survive iterated elimination of dominated strategies form a regular set.

Zielonka's theorem shows that each regular set of Mazurkiewicz traces can be implemented as a system of synchronized processes provided with some distributed control structure called an asynchronous automaton. This paper gives a new algorithm for the synthesis of a non-deterministic asynchronous automaton from a regular Mazurkiewicz trace language. Our approach is based on a simple unfolding procedure that improves the complexity of Zielonka's and Pighizzini's techniques: Our construction is polynomial in terms of the number of states but still double-exponential in the size of the alphabet.

Dans cet exposé, nous montrons que les séries génératrices des systèmes dynamiques polynomiaux sont exactement les mêmes que les séries génératrices d'une sous-classe de réseaux de Petri pondérés, dans lesquels chaque transition a une seule place d'entrée avec un poids de l'arc égal à 1. Nous proposons ensuite un algorithme pour vérifier si un reseau de Petri donné correspond directement à un système dynamique. Dans de nombreux cas des marquages initiaux différents correspondent a des systèmes dynamiques différents. Nous montrons enfin que les invariants de places dans les réseaux de Petri correspondent aux symétries de Lie de changement d'échelle du système dynamique correspondant, ainsi que les invariants du groupe de symétrie du système dynamique correspondent aux places implicites de réseau de Petri correspondant.

Le concept de L-système a été introduit par Lyndenmayer dans les années soixante pour la modélisation du vivant et plus particulièrement de végétaux. D'un point de vue abstrait, il s'agit essentiellement de réÂécritures parallèles. Depuis, de nombreux développements ont vu le jour sous la forme par exemple de M0L-systèmes ou encore de grammaires BNLC parallèles.

Dans cet exposé, on s'intéressera aux D0L-systèmes (L-systèmes déterministe indépendant du contexte) de graphes et d'arbres. Nous montrerons que ces systèmes ont des propriétés algorithmiques robustes: la logique monadique du second ordre est décidable pour une famille d'arbre engendrée par un D0L-système. Pour les graphes, la situation est un peu plus compliquée, néanmoins on montre que la logique du premier ordre d'une famille de graphe engendrée par un D0L-système est décidable.

Model checking based on Petri net unfoldings is an approach widely applied to cope with the state space explosion problem. In this paper, we propose a new condensed representation of a Petri net's behaviour called merged processes, which copes well not only with concurrency, but also with other sources of state space explosion, viz. sequences of choices and non-safeness. Moreover, this representation is sufficiently similar to the traditional unfoldings, so that a large body of results developed for the latter can be re-used. Experimental results indicate that the proposed representation of a Petri net's behaviour alleviates the state space explosion problem to a significant degree and is suitable for model checking.

Cet exposé porte sur la vérification de systèmes modélisables par des automates communicants (CFSM). La difficulté est que, dans ce modèle, l'atteignabilité est indécidable si on ne borne pas la taille des files. Tout d'abord, nous présenterons "l'état de l'art" : les techniques d'accélération qui permettent, dans certains cas, de calculer l'ensemble des états atteignables. Puis nous nous intéresserons à la mise en oeuvre d'une analyse de type "interprétation abstraite". Dans ce cadre, nous serons amenés à définir un opérateur d'élargissement pour le treillis des langages réguliers.

Nous considérons dans cet exposé une extension des expressions oméga-régulières. Dans ces expressions, en plus de l'étoile de Kleene, deux autres opérateurs d'itération sont possibles, nommément ^B et ^S. Leur sémantique ressemble à celle de l'étoile, mais de plus contraint le nombre d'itérations à être borné (pour B) ou à tendre vers l'infini (dans le cas de S).
Par exemple (a^B.b)^omega représente l'ensemble des mots infinis contenant une infinité de `b' pour lesquels les séquences de `a' consécutifs sont bornées.

Nous présenterons ces langages et étudierons leurs propriétés (expressivité, décidabilité, clôture). Nous appliquerons ensuite ces résultats pour montrer la décidabilité d'un fragment de logique étendant la logique monadique du second ordre.

Il s'agit d'une collaboration avec Mikolaj Bojanczyk.

An interactive synthesis of asynchronous circuits from Signal Transition Graphs (STGs) based on partial order semantics is presented. In particular, the fundamental problem of encoding conflicts in the synthesis is tackled, using partial orders in the form of STG unfolding prefixes. They offer a compact representation of the reachable state space and have the added advantage of simple structures.
Synthesis of asynchronous circuits from STGs involves resolving state encoding conflicts by refining the STG specification. The refinement process is generally done automatically using heuristics. It often produces sub-optimal solutions, or sometimes fails to solve the problem, then requiring manual intervention by the designer. A framework for an interactive refinement process is presented, which aims to help the designer to understand the encoding problems. It is based on the visualisation of conflict cores, i.e. sets of transitions causing encoding conflicts, which are represented at the level of finite and complete prefixes of STG unfoldings. The refinement includes a number of different transformations giving the designer a larger design space as well as applying to different levels of interactivity. This framework is intended to work as an aid to the established state-based synthesis. It also contributes to an alternative synthesis based on unfolding prefixes rather th an state graphs.
The proposed framework has been applied to a number of design examples to demonstrate its effectiveness. They show that the combination of the transparent synthesis together with the experience of the designer makes it possible to achieve tailor-made solutions.

http://async.org.uk/

Time Petri nets have proved their interest in modeling real-time concurrent systems. Their usual semantics is defined in term of firing sequences, which can be coded in a (symbolic and global) state graph, computable from a bounded net.
An alternative is to consider a ``partial order'' semantics given in term of processes, which keep explicit the notions of causality and concurrency without computing arbitrary interleavings. In ordinary place/transition bounded nets, it has been shown for many years that the whole set of processes can be represented by what is called the ``unfolding''. We define a symbolic unfolding for safe time Petri nets using a concurrent operational semantics.

http://www.inria.fr/rrrt/rr-5706.html

We define a symbolic determinisation procedure for a class of infinite-state systems, which consists of automata extended with symbolic variables that may be infinite-state.

The subclass for which the procedure terminates is characterized as {\em bounded-lookahead} extended automata, for which the observation of a finite trace allows to infer the first action actually taken. We discuss applications of the algorithm to the verification, testing, and diagnosis of infinite-state systems.

(This is joint work with Thierry Jeron and Herve Marchand)

Nous proposons un langage de programmation simple, appelé Nemo, spécifique au domaine des systèmes de contrôle-commande temps-réel multi-tâches, tels qu'on les trouve dans les systèmes robotiques, automobiles ou avioniques. Ce langage permet de spécifier un ensemble de ressources avec des contraintes d'utilisation, un ensemble de tâches qui les consomment selon divers modes, et des applications qui séquencent les tâches. Nous obtenons automatiquement un gestionnaire de tâches, spécifique à l'application, qui traite correctement les contraintes (s'il en existe un), au moyen d'un processus de compilation comprenant une phase de synthèse de contrôleurs discrets. De cette façon, cette technique formelle contribue à la sûreté des systèmes ainsi conçus, tout en étant encapsulée dans un outil qui la rend utilisable par les spécialistes des applications. Nous nous plaçons dans le cadre des techniques de modélisation, langages et outils synchrones.

http://www.inria.fr/rrrt/rr-5690.html

Quelle confiance accorder à un compilateur? Comment savoir que le code machine produit se comporte comme prescrit par la sémantique du programme source? La question est particulièrement importante pour le logiciel critique, dont le code source est certifié à l'aide de méthodes formelles, et pour lesquels tout bug dans le compilateur peut invalider la certification. Plusieurs solutions à ce problème ont été proposées, notamment le code auto-certifié (proof-carrying code) et la validation de traducteurs. L'approche la plus directe est la certification formelle du compilateur lui-même, vu comme un programme critique: on cherche à prouver sur machine un résultat de préservation de la sémantique entre le code source fourni et le code machine produit. Avec l'aide des membres de l'ARC Concert, j'ai réalisé une telle preuve, en Coq, d'un back-end de compilateur modérément optimisant, qui traduit Cminor (un langage intermédiaire impératif de bas niveau) en assembleur PowerPC. Une originalité de ce travail est que l'essentiel du compilateur est programmé directement dans le langage de spécification de Coq, puis extrait automatiquement vers du code Caml exécutable. L'exposé présentera une vue d'ensemble de ce compilateur et de sa (très grosse) preuve en Coq, et tirera quelques leçons de cette expérience.

Les systèmes à événements discrets modulaires (aussi dit concurrents) sont formés par une collection de modules (sous-systèmes locaux). Le système (automate) global est obtenu par produit synchrone des modules. De plus, les événements locaux ne sont pas tous observables, mais ils sont composés des événements observables et inobservables. Nous allons présenter des méthodes pour calculer les superviseurs optimaux (i.e. les moins restrictifs) sans le recours à la construction du système globale. Nous considérerons les cas où la spécification est décomposable en spécifications locales et le cas où elle est indécomposable.

We clarify the notion of architecture in decentralized control, in order to consider the realizability problem: given a discrete-event system, a desired behavior and an architecture for a decentralized control, can the desired behavior be achieved by decentralized controllers obeying the given architecture? We investigate this problem for any mu-calculus definable behavior and for a large family of architectures. The method consists in compiling into a single mu-calculus formula both the desired behavior and the desired architecture. Applications of this approach are first a single synthesis algorithm of decentralized controllers (with total observation) for the whole presented family of architectures, and second, an adequate mathematical framework to compare different architectures.

Nous proposons un algorithme symbolique efficace pour vérifier qu'une propriété globale, spécifiée par un moniteur, est satisfaite par une exécution d'un système distribué asynchrone. Le problème se réduit au model-checking de traces de Mazurkiewicz finies. On montre que le problèmes est NP-complet et propose une méthode de réduction qui s'inspire du principe des techniques de réduction par ordre partiel qui essaye d'éviter d'explorer l'ensemble des entrelacements possibles. Nous montrons que notre méthode peut supprimer un facteur exponentiel dans l'exploration comparés à l'exploration classique avec ou sans réduction par ordre partiel. En pratique, notre méthode est efficace.

On introduit le problème de distribution de code statique. Ce problème est rencontré lors de la production de code performant pour le langage dSL, langage qui possède des mécanismes permettant la distribution transparente de code, pour la programmation de contrôleurs industriels. On présente d'abord brièvement ce langage, pour ensuite formaliser le problème de production de code efficace. Ce problème est montré équivalent au problème NP-Complet appelé "Multiterminal cut". Le mutliterminal cut est un cas généralisé du ST- cut. Le fameux théorème Max-Cut/Min-Flow, démontré par Ford et Fulkerson, a mené à un algorithme polynomial résolvant le ST-Cut. Dans l'exposé, on montre comment la taille d'une instance du Multiterminal Cut peut être réduite en utilisant des ST-cut. Cette opération est appelée "shrinkage", et était introduit par Dhalhaus et al. Dans notre travail, on généralise cette méthode de shrinkage, de façon à pouvoir obtenir une réduction plus importante. Ensuite on iWe clarify the notion of architecture in decentralized control, in order to consider the realizability problem: given a discrete-event system, a desired behavior and an architecture for a decentralized control, can the desired behavior be achieved by decentralized controllers obeying the given architecture? We investigate this problem for any mu-calculus definable behavior and for a large family of architectures. The method consists in compiling into a single mu-calculus formula both the desired behavior and the desired architecture. Applications of this approach are first a single synthesis algorithm of decentralized controllers (with total observation) for the whole presented family of architectures, and second, an adequate mathematical framework to compare different architectures.ntroduit une série d'observations nouvelles sur le ST-Cut qui mènent à une nouvelle heuristique efficace et performante pour le Multiterminal Cut.

Dans cet exposé, nous présentons une extension des résultats de Badouel & Darondeau sur la synthèse de réseaux de Petri non étiquetés à partir d'un langage régulier au cas d'une famille de langages solutions de formules de mu-calcul modal; ces formules sont traduites en spécifications modales, dont une restriction structurelle rend le problème décidable.

We will present tag systems, a mathematical framework in which the composition of heterogeneous reactive systems can be analysed. Our framework encompasses diverse models of computation and communication such as synchronous, asynchronous, causality-based partial orders, earliest execution times, and more. Our theory allows to establish theorems, from which design techniques for correct-by-construction deployment of abstract specifications can be derived. An operational view of tagged systems will then be presented: we will present tag machines, that act as finite generators of tagged systems. Properties of tag machines are investigated. A fundamental theorem on compositionality is given as a first step towards effective design methods for heterogeneous systems.

Dans cet exposé, nous nous intéressons à la vérification d'un système distribué en de nombreux processus asynchrones a priori inconnu mais observable. Le but est de vérifier une formule logique globale concernant l'ensemble des prédicats observables locaux à chacun des processus.

Pour cela, un superviseur est associé à chacun des processus p, et peut ajouter de l'information aux messages envoyés au processus q, information qui sera reçue par le superviseur du processus q. Le but est que au moins un superviseur soit capable de savoir un jour si une suite d'opérations interdite par la formule a été exécutée, ou mieux soit capable de le savoir immédiatement. Nous ne nous intéressons pas à contrôler le système, c'est à dire que les superviseurs ne peuvent pas influer sur ce que font les processus (autre que éventuellement faire retentir une alarme ou arrêter le système).

Les superviseurs peuvent donc observer puis informer les autres superviseurs, ce qui correspond à ce que font les processus dans la construction de Zielonka. Nous éclaircirons les relations entre les deux problèmes, et donneront ainsi la complexité de différentes variantes connues et nouvelles du théorème de Zielonka qui permettent aussi d'accomplir la vérification dynamique distribuée.

Cet exposé regroupe plusieurs travaux, certains en collaboration avec Anca Muscholl, Peter Niebert et Doron Peled.

Pages hébergées à l'Irisa. En cas de problèmes, nous contacter.