EXPOSES 2000-2001
Retour à la page du séminaire
Transparents des séminaires

Nous proposons un cadre très général pour l'étude des Problèmes de Contrôle de Systèmes (d'Etats Finis) à Evénements Discrets : nous montrons comment la plupart des énoncés d'existence d'une solution à un problème de contrôle se réduit à un problème de Model-Checking dans une Logique Temporelle ``Quantifiée'' (au sens de la quantification sur les propositions atomiques). On établira de plus que l'algorithme de Model-Checking est constructif, au sens où la preuve d'existence d'un contrôle adéquat au problème est effective.

McMillan's unfolding approach to the reachability problem in 1-safe Petri nets and its later improvements by Esparza-Römer-Vogler have proven in practice as a very effective method to avoid state-explosion. This method computes a complete finite prefix of the infinite branching process of a net. On the other hand, the Local First Search approach (LFS) was recently introduced as a new partial order reduction technique which characterizes a restricted subset of configurations that need to be explored to check local properties. In this paper we amalgamate the two approaches: We combine the reduction criterion of LFS with the notions of an adequate order and cutoff events essential to the unfolding approach. As a result, our new LFS method computes a reduced transition system without the problem of state duplication (present in the original LFS). Since it works for any transition system with an independence relation, this black box partial unfolding remains more general than the unfolding of Petri nets. Experiments show that the combination gives improved reductions compared to the original LFS.

TRANSPARENTS (POSTSCRIPT)

Une communauté intentionnelle est un regroupement de programmes partageant et s'adaptant à un contexte qui les imprègne tous. Le contexte est un point dans un espace multidimensionnel et la sémantique de ces programmes est donnée en utilisant les mondes possibles de la logique intentionnelle. Le contexte peut évoluer de lui-même ou par l'action d'un des programmes, résultant en un système privilégiant la diffusion plutôt que la communication point-à-point.
L'implantation d'une communauté intentionnelle se fait à l'aide d'un serveur de contextes mis en réseau, qui permet la rediffusion des changements de contexte à l'ensemble des programmes dans la communauté. Les programmes eux-mêmes sont écrits dans un langage de programmation sensible au contexte.
Dans cette présentation, nous donnons non seulement les concepts et la sémantique des communautés intentionnelles, mais nous les illustrons avec un ensemble de pages Web sensibles au contexte (langue d'interface, niveau de détail, taille d'image, ...). Quand le contexte est changé, la page est régénérée et les liens entre les pages sont créées de manière dynamique. Plusieurs personnes peuvent naviguer le Web ensemble, chacun ayant ses préférences personnelles.

http://www.cse.unsw.edu.au/school/people/info/plaice.html

Les techniques automatiques mises en ouvre pour valider les systèmes concurrents sont fortement contraintes par la taille de leur espace d'états. Fort heureusement, la recherche de fonctionnements symétriques au sein de ces systèmes permet de combattre ce problème de façon efficace, en définissant des relations d'équivalence entre les états. Des expériences concrètes et positives ont été démontrées tant dans le cadre de l'évaluation de performances (chaîne de Markov) que de la vérification de modèles (model checking).
Une recherche menée conjointement avec Serge Haddad de l'université Paris Dauphine, a permis d'étendre à leur paroxysme le concept de symétries. Nous définissons localement et à la volée les symétries exploitables en chaque point d'analyse de l'espace d'états. Pour simplifier, nous limiterons cette présentation aux logique temporelle à temps linéaire (LTL, automate de Büchi), pour lesquelles un outil de validation est en cours de construction au sein du laboratoire Lip6. Ce dernier combine les optimisations obtenues avec d'autres plus traditionnelles.

1 - J.M. Ilié, S.Haddad, « Symétries et logique temporelle », sous la direction de Michel Diaz, chapitre 14 du livre 'les réseaux de Petri', 20 pages, à paraître chez Hermes en 2002.
2 - S.Haddad, J.M. Ilié, K. Ajami, "A Model Checking Method for Partially Symmetric Systems", dans les actes de FORTE'00, Pise - Italy, oct, 2000.
3 - L. Capra, C. Dutheillet, G. Franceschinis and J-M. Ilié, « Exploiting Partial Symmetries for Markov Chain Aggregation », Electronic Notes in Theoretical Computer Science, vol. 39-3, Elsevier Science Publishers, déc. 2000. Aussi dans les actes de MTCS'2000, « first int. workshop on Models for Time-Critical Systems » en association avec Concur 2000, Pennsylvania, USA, 26 Aout 2000.
TRANSPARENTS (PowerPoint)

We consider a new class of infinite graphs defined as the smallest solution of equational systems with vertex replacement operators and unsynchronised product. We show that those graphs have an equivalent internal representation as graphs of recognizable ground term rewriting systems. Furthermore, we show that, when restricted to bounded tree-width, those graphs are isomorphic to hyperedge replacement equational graphs. Finally, we prove that on a wider family of graphs --- interpretations of trees having a decidable monadic theory --- the first order theory with reachability is decidable.

TRANSPARENTS (POSTSCRIPT)

Nous nous intéressons à l'analyse d'invariants et à la vérification de programmes réactifs manipulant différents type de données (booléens, réels, files d'attente, ...).
Nous proposons dans ce cadre une solution pour combiner efficacement ces différents types de donnée dans le cadre de l'interprétation abstraite. Celle-ci repose sur une notion très générale de partitionnement en interprétation abstraite, une méthode de calcul approchés de transformateurs de prédicats et des heuristique de raffinement de partition.
Nous présenterons ces différents aspects, et illustrerons l'efficacité pratiques de nos solutions sur des études de cas.

Plutôt que d'utiliser des grammaires ou des machines d'acceptation pour définir des familles de langages, il est apparu plus naturel de les caractériser par transformations rationnelles à partir de systèmes générateurs. Dans les années soixante, Ginsburg et Greibach ont proposé la notion d'AFL (Abstract Family of Languages) pour généraliser ce concept. La même démarche appliquée aux graphes infinis nous a amenés à définir la notion d'AFG principal (Abstract Family of Graphs) dont les traces sont des AFL. Dans cet exposé, nous dresserons un parallèle entre familles de langages et familles de graphes.

TRANSPARENTS (FICHIER PDF)

- J.-M. Autebert and L. Boasson, "Transductions Rationnelles -- Application aux Langages Algébriques", Masson, 1988
- W. Thomas "A Short Introduction to Infinite Automata", to appear in Proc. DLT 2001, LNCS, Springer-Verlag 2002.
http://www-i7.informatik.rwth-aachen.de/~thomas/papers/infaut2.ps

Les automates cellulaires sont un modèle de parallélisme mettant l'accent sur une uniformité et une homogénéité de structure. Cela ne pose pas de problème particulier sur la droite où l'on n'a guère de définition possible, sauf à varier la taille du voisinage d'une cellule. Dans le cas du plan, plusieurs solutions apparaissent naturellement. Et, du fait de l'homogénéité rappelée ci-dessus, les automates cellulaires du plan sont traditionnellement étudiés sur les pavages réguliers du plan euclidien, un peu dans l'espace à trois dimensions aussi. Il y a eu quelques travaux sur des cas plus généraux, faisant appel aux graphes de Cayley. Dans l'exposé, on s'intéressera à une nouvelle méthode que j'ai introduite en 1998 dans un travail commun avec Kenichi Morita, adaptée plus spécifiquement à un pavage particulier du plan hyperbolique, celui du pentagone régulier à angles droits. J'ai depuis perfectionné cette méthode qui s'applique à bien d'autres pavages de ce plan (il y en a une infinité) en ce qu'on pourrait qualifier de proposition pour une approche combinatoire de la géométrie hyperbolique. La méthode s'applique aussi à un pavage de l'espace hyperbolique à trois dimensions, le pavage du dodécaèdre régulier à angles droits.

La conception des systèmes robotiques et de contrôle-commande est de plus en plus difficile, ainsi que leur programmation et leur opération. Ceci est dû à leur taille et complexité grandissante. C'est pour cela que leurs architectures de programmation et exécution temps-réel requierrent plus d'assistance à l'utilisateur et au concepteur, foncée sur des abstractions utilisables et le support d'outils. Les méthodes formelles peuvent être utiles, particulièrement dans les systèmes de contrôle de sécurité critique (par ex., la robotique spatiale ou chirurgicale), mais elles doivent être rendues utilisables par des spécialistes du domaine d'application. Des langages et interfaces dédiés aux utilisateurs facilitent l'usage de techniques d'analyse et mise en oeuvre temps-réel. Nous nous intéressons particulièrement à la programmation au niveau tâche en robotique et contrôle-commande, où les tâches encapsulent les lois de commande. Nous considérons l'application de techniques de synthèse de contrôleurs discrets, intégrées dans le cadre d'un environnement de programmation au niveau tâche~: elles permettent la génération automatique de contrôleurs corrects pour des applications de contrôle-commande. Nous utilisons l'environnement de programmation synchrone Signal, et l'outil de vérification et synthèse Sigali. Ceci requiert la définition de motifs de tâches et d'objectifs, qui soient à la fois spécifiques au domaine du contrôle-commande, et suffisamment génériques pour couvrir une large classe de systèmes de contrôle. Nous considérons une application à la téléopération discrète sûre. Nous illustrons ceci par une étude de cas concernant le contrôle interactif discret des tâches du système d'excavation.

Étant donné une contrainte linéaire sur les vecteurs comptant les tirs d'actions d'un graphe marqué vivant (borné ou non borné) ayant des transitions inobservables / incontrôlables, on calcule le contrôleur le plus permissif qui en assure le respect, en utilisant la dualité linéaire dans le cas particulier des matrices totalement unimodulaires. L'originalité réside entre autres dans le traitement des actions inobservables: on peut les éliminer en projetant le graphe marqué vivant sur un autre graphe marqué vivant totalement observable. A la différence du contrôle par moniteurs, les contrôleurs résultants sont de complexité polynomiale. Dans le cas des graphes marqués vivants et fortement connexes, on aborde aussi la question du contrôle le plus permissif assurant le respect de la contrainte en préservant la vivacité. Ce problème peut être réduit par projection à un problème classique sur les automates finis, ce qui n'amène pas de nouveaux résultats de complexité. Le cadre géométrique dans lequel le problème est posé devrait pourtant permettre d'employer des méthodes symboliques restant à définir.

A central problem with stack inspection is to determine to what extent the local checks inserted into the code are sufficient to guarantee that a global security property is enforced. In this paper, we present a technique for inferring a secure calling context for a method. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. This is particularly useful for annotating library code in order to avoid having to re-analyze libraries for every new application. The technique is a constraint-based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.

Ce travail a démarré par une requête des ingénieurs de la société Telelogic Technologies Toulouse (TTT) qui développent l'environnement SCADE. Leurs clients, utilisateurs de SCADE, souhaitent en effet pouvoir décrire certaines parties de leurs programmes par des graphes d'états. Les ingénieurs de TTT proposaient d'attacher des équations LUSTRE aux états d'un automate.
Nous avons comparé ces besoins à ce qu'offrait l'approche par édition de liens de programmes LUSTRE et ARGOS, sur laquelle le laboratoire Vérimag travaille depuis 1993. Nous avons identifié, dans les besoins des utilisateurs de SCADE, la notion de mode de fonctionnement, qui semble difficile à décrire avec les approches suivies jusque là dans la combinaison de langages synchrones. Nous avons cherché dans la littérature cette notion de mode de fonctionnement. On trouve de nombreuses références à des modes, mais aucune des approches ne correspond exactement à nos besoins. Ces constatations justifient donc l'étude d'une nouvelle construction spécifique pour décrire les modes de fonctionnement, dans un langage flot de données comme LUSTRE.
Nous avons défini les automates de modes et nous leur avons donnés une sémantique précise. Pour pouvoir essayer cette construction nous avons réalisé une traduction simple en LUSTRE des automates de modes. Les différents essais que nous avons réalisés montrent que cette construction correspond effectivement aux besoins des utilisateurs.
L'étape suivante de notre travail a été de définir la traduction des automates de modes non plus en LUSTRE, mais en DC (un format interne de la chaîne de compilation de LUSTRE vers C). L'implantation de cette traduction a été achevée pour les automates de modes utilisant un sous-ensemble du langage LUSTRE dans les équations. Cette réalisation nous permet d'utiliser les automates de modes sur des études de cas de taille importante.
La présentation montrera les différentes étapes de cette étude, de puis les motivations jusqu'à la mise en oeuvre pratique dans le compilateur MATOU.
http://www-verimag.imag.fr/~remond/

L'étude de la relation entre syntaxe et sémantique qu'établissent les grammaires de types logiques a essentiellement privilégié le sens de l'analyse - syntaxe vers sémantique. Nos travaux soulignent le profit que la génération - sémantique vers syntaxe - tire de l'étroitesse de cette relation.
Elle s'appuie sur l'étude logique de ces modèles grammaticaux et met en avant l'utilisation de la logique linéaire et de ses réseaux de preuve. L'utilisation de ces réseaux nous permet de montrer que, pour le calcul de Lambek et pour des représentations sémantiques linéaires avec une constante au moins, le problème de génération est décidable et que ces grammaires sont intrinsèquement réversibles. Nous caractérisons les formes sémantiques permettant une réalisation syntaxique polynomiale.
http://www.xrce.xerox.com/people/pogodalla

Ideal reuse is a myth. It is hardly achieved. In general few components are reused as they are. Often, available components are incompatible with what is required - and still we want to reuse them. This necessitates extensions or adaptations. In this seminar I report on work developing algorithms for the synthesis of adapters, coercing incompatible components into meeting requirements. These adapters lead to a concept of normalized software architectures where adapters handle common synchronization problems between components. I will also briefly sketch the broader project context of this research.
http://www.csse.monash.edu.au/~hw
http://www.csse.monash.edu.au/dsse

Efficiently compiling large Esterel programs remains an open problem, and existing Esterel compilers are not open-source, hindering research on the topic. This is a a work-in-progress description of a new open-source Esterel compiler I am currently developing. I describe its internal database and a new intermediate representation, as well as proposals for new code generation techniques. My hope is that this framework will further research on compiling this interesting language.

Nous présentons une approche de génération automatique de séquences de tests aux limites à partir d'un modèle formel B ou Z appelée BZ-Testing-Tools. Les tests générés satisfont un critère de couverture des spécifications aux limites. Cela ce traduit dans la méthode BZ-Testing-Tools par l'extraction, à partir du modèle formel, d'états limites dans lesquels le système est placé par parcours du graphe d'atteignabilité contraint. Le système étant dans cet état aux limites, l'idée est de tester l'ensemble des opérations actives (qui modifient les variables d'état) activables avec l'ensemble des valeurs limites des variables d'entrée pour ces opérations. Cette méthode est totalement supportée par l'environnement BZ-Testing-Tools dont le pivot est le solveur de contraintes logico-ensemblistes CLPS/BZ. La méthode et l'environnement ont été validés dans le cadre de trois collaborations industrielles dans le domaine du logiciel critique : la norme Smart Card GSM 11-11, l'algorithme de validation de tickets de transport et le mécanisme des transactions de la Java Card Virtual Machine. Ces mises en oeuvre sur des applications réelles ont montré d'une part la qualité de la couverture des test générés, d'autre part la réduction d'effort apportée par l'approche dans la conception des tests (modélisation formelle incluse) et enfin l'exécutabilité et l'observabilité des tests générés.

http://lib.univ-fcomte.fr/libhome.html
http://lib.univ-fcomte.fr/RECHERCHE/TFC/Page_Web_Activite_Contrainte.html

TRANSPARENTS (FICHIER PDF)

Les systèmes de réécriture sont des outils formels classiques et relativement tout-terrains: ils sont utilisés aussi bien comme moteur de simplification dans les démonstrateurs, que comme sémantique opérationnelle dans certains langages de programmation, etc. Ils peuvent être également utilisés comme outil de modélisation de programmes. Dans ce cas, il est possible de prouver des propriétés sur le programme modélisé en prouvant des propriétés sur le système de réécriture associé. Cependant, les outils de preuve en réécriture requièrent tous la terminaison du système de réécriture.
Si le système ne termine pas (ou si la preuve de terminaison est trop complexe), il est malgré tout possible de prouver des propriétés en calculant une sur-approximation de l'ensemble des termes atteignables par réécriture (les descendants). En particulier, à l'aide de cette sur-approximation il est possible de prouver que certains ensembles de termes, représentant des situations critiques par exemple, sont inatteignables.
Nous présentons Timbuk -- une librairie d'automates d'arbres -- qui implante les opérations habituelles sur les automates d'arbre ainsi qu'un algorithme de complétion permettant de calculer une sur-approximation de l'ensemble des descendants. Nous verrons également, sur quelques exemples pratiques venant du monde des protocoles cryptographiques, comment définir simplement des règles d'approximation.

Dans cet exposé on démontrera l'équivalence entre les traces des graphes rationnels et les langages contextuels.
http://www.morvan.fr.st/ et les TRANSPARENTS (FICHIER PDF)

Les réseaux de Petri ont été, à ma connaissance, le premier modèle théorique augmenté d'aspects temporels quantitatifs. De nombreux modèles ont été développés depuis 25 ans, associant des dates ou des intervalles de tir aux transitions, places ou arcs, avec ou sans urgence. Dans cet exposé, je ferai une présentation des principaux modèles (en laissant de côté les aspects stochastiques) et de leurs pouvoirs d'expression relatifs.
http://liafa.jussieu.fr/~boyer/

[J'ai récemment passé mon HDR à l'Université de Nantes où je suis actuellement en détachement et suis heureux de refaire l'exposé à Rennes, d'autant que ces travaux sont davantage issus de mon séjour à l'IRISA que de ma récente intégration à l'IRIN.]

Après avoir brièvement présenté les deux domaines concernés, nous montrerons comment la logique linéaire non commutative (ou calcul de Lambek) modélise l'analyse syntaxique par la construction de déductions formelles. On soulignera les deux avantages principaux de cette approche: d'une part l'algorithme qui extrait des analyses syntaxiques les représentations sémantiques (des formules du premier ordre), et d'autre part l'algorithme d'inférence grammaticale, qui, à partir d'exemples, construit automatiquement de telles grammaires. Puis nous en viendrons à nos contributions qui s'inscrivent dans cette approche.

Côté logique, les réseaux de démonstration, qui relèvent de la théorie des graphes standard (cographes, couplages), permettent d'avoir une correspondance bijective entre analyses syntaxiques et démonstrations formelles, et aussi d'étendre la logique.

Côté grammatical, les variantes non commutatives de la logique linéaire et la syntaxe des réseaux de démonstration permettent de définir de nouveaux modèles grammaticaux plus riches et linguistiquement mieux fondés, qui rendent compte des grammaires d'arbres adjoints ou du récent programme minimaliste de Chomsky.

On conclura sur les perspectives du domaine.
http://perso.wanadoo.fr/retore/christian

We consider three natural classes of infinite-state HMSCs: transition-connected, transition-synchronized and local-choice HMSCs. We show first that model-checking for transition-connected and transition-synchronized HMSCs is of the same complexity as for the restricted class of bounded (regular) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient than for transition-synchronized HMSCs. We also show that transition-synchronized and local-choice HMSCs are always implementable by communicating finite-state machines with additional (finite) memory. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.

TRANSPARENTS (FICHIER POSTSCRIPT)

Applying formal methods to testing has recently become a popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use test generation techniques to extract subgraphs (called "components") from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification. We demonstrate the approach by verifying an electronic purse system using our symbolic test generation tool STG and the PVS theorem prover.
http://www.irisa.fr/pampa/perso/rusu/draft/

Presence and absence of signals inside a reaction are inherent to the synchronous paradigm, as well as clocks which are sets of instants that indicate when a given condition is fulfilled over a sequence of reactions (e.g. when a signal is present). Clocks are essential to capture the control in data-flow specifications; more generally relations between clocks should be analyzed to detect e.g. inconsistencies and verify some properties. These relations express particular safety properties many of which can be verified without considering the dynamic of systems, by means of a static abstraction. We propose a language CL to describe such properties and prove it decidable. Finally, model-checking is derived for e.g. Signal programs, on the basis of a translation from the static abstraction of Signal into CL.
http://www.irisa.fr/prive/mnebut/

Message sequence charts and high-level message sequence charts are popular formalisms for the specification of asynchronous communicating processes. An important conceptional component in this context are channel buffers between communicating processes. We view the size of these buffers as a computational resource similar to space in classical computing devices. We introduce four different measures for buffer sizes and investigate for each of these measures the complexity of deciding whether a given (high-level) message sequence chart satisfies a given bound on the buffer size. The complexity of these problems varies between the classes P, NP, and coNP.

Dès son développement, le mu-calcul a été reconnu comme une puissante logique de programmes. Il atteint la puissance d'expression de la logique au deuxième ordre monadique MSO sur les mots et sur les arbres. Appliqué aux systèmes de transition, le mu-calcul subsume la plupart des variantes connues de logiques dynamiques et temporelles, et capture exactement les propriétés en MSO qui sont fermées par bisimulation. De plus, le mu-calcul dispose d'un algorithme élémentaire de décision (simple exponentiel) et il admet un système naturel de preuves. Cependant, quelques questions intéressantes de décidabilité restent posées, en particulier au sujet du mu-calcul sur des systèmes de transition infinis comme les arbres à pile d'ordre supérieur. Des travaux récents ont montré un lien intrinsèque entre le mu-calcul et des jeux infinis avec information complète. Le mu-calcul, particulièrement dans sa forme booléenne, peut être vu comme un formalisme combinatoire qui transpose des problèmes de vérification en des problèmes de nature algorithmique : celui de déterminer un gagnant dans un jeu de parité. Cependant, la complexité exacte de ce problème (NP et co-NP) reste une question ouverte.

On peut s'attendre pour les années a venir a un développement important des systèmes logiciels utilisant le concept de code mobile. Ces systèmes posent des problèmes nouveaux de développement par rapport aux systèmes distribues actuels. En particulier, le test de tels systèmes doit prendre en compte la mobilise des processus testes qui rend difficile le maintien des points de contact entre processus testeurs et testes et la nature embarque du processus sous test dans son environnement d'exécution. Nous présentons ce problème et proposons une solution fondée sur la simulation des systèmes de processus mobiles, et l'intégration des processus testes dans un simulateur. Le développement d'un tel simulateur nécessite d'abstraire le modèle d'exécution des différentes plates-formes de processus mobiles pour en déduire une implémentation générique. Enfin, il faut aussi définir un mécanisme d'observation dynamique pour exprimer et exécuter les tests. La présentation sera suivie d'une petite démonstration (environ 10 min) sur un exemple.

Nous nous intéressons à l'analyse de Processus de Décision Markoviens, qui sont des processus offrant à la fois des choix indéterministes et des choix probabilistes. Nous souhaitons plus spécifiquement vérifier sur ces processus des propriétés dites d'accessibilité, du type: "quelle est la probabilités minimale (resp. maximale) d'atteindre un ensemble d'états finaux à partir d'un ensemble d'états initiaux au cours d'une exécution ?" Afin de contourner la complexité élevée d'une telle analyse, nous proposons d'abstraire le système à vérification de façon à préserver la propriété à vérifier, de mener l'analyse sur le système abstrait, et de raffiner automatiquement l'abstraction tant que celle-ci ne permet pas de décider si la propriété est vraie ou fausse. Nous commencerons par présenter le modèle des Processus de Décision Markoviens, puis nous décrirons la relation d'abstraction que nous avons définie, avant de présenter les algorithmes implantés dans un outil prototype et les résultats expérimentaux que nous avons obtenus.
http://www-verimag.imag.fr/~bjeannet/djjl01.html

The synthesis of controllers for discrete event systems, as introduced by Ramadge and Wonham, amounts to computing winning strategies in parity games. We show that in this framework it is possible to extend the specifications of the supervised systems as well as the constraints on the controllers by expressing them in the modal --calculus. In order to express unobservability constraints, we propose an extension of the modal --calculus in which one can specify whether an edge of a graph is a loop. This extended --calculus still has the interesting properties of the classical one. In particular it is equivalent to automata with loop testing. The problems such as emptiness testing and elimination of alternation are solvable for such automata. The method proposed in this paper relies on a simple construction of the quotient of automata with loop testing by a deterministic transition system. This is enough to deal with the centralized control problems. The solution of the decentralized control problems uses a more involved construction of the quotient of two automata. This work extends the framework of Ramadge and Wonham in two directions. We consider infinite behaviours and arbitrary regular specifications, while the standard framework deals only with specifications on the set of finite paths of processes. We also allow dynamic changes of the set of observable and controllable events.

Afin de développer des techniques de vérification formelle de systèmes infinis, il est indispensable de déterminer la frontière entre le décidable et l'indécidable dans ce domaine. On s'intéresse à la logique au deuxième ordre monadique puisqu'elle généralise la plupart des logiques temporelles et des logiques de programmes. Par ailleurs, on s'intéresse aux arbres à partir desquels on peut construire des systèmes de transition par des techniques préservant la décidabilité de la théorie monadique. Un système d'équations d'arbres est de niveau 0 si toutes ses inconnues sont de type de base. La plus petite solution d'un système de niveau 0 est un arbre régulier dont la décidabilité de la théorie monadique découle du théorème de Rabin. Un système d'équations est de niveau 1 s'il possède des inconnues de type fonctionnel avec des paramètres de type de base. De tels systèmes correspondent aux schémas de programmes récursifs. Leurs solutions sont les arbres algébriques. La décidabilité de leur théorie monadique a été établie en 1995 par Courcelle. Si on autorise des objets de type fonctionnel parmi les paramètres, on obtient les équations de niveau 2 dont les solutions sont des arbres hyper-algébriques. Dans cet exposé, nous discuterons de la décidabilité de la théorie monadique des arbres hyper-algébriques.

Nous nous intéressons ici à une nouvelle classe de problèmes de commande optimale. Pour cela, nous adoptons le formalisme à la Ramadge & Wonham et modélisons le système à contrôler comme étant le langage marqué généré par une machine à états finis. Le problème du contrôle considéré est similaire à celui de Ramadge & Wonham et se caractérise par la présence d'événements incontrôlables et la notion de fonction de coûts sur les événements. Toutefois, par rapport aux travaux de [Sengupta & lafortune Siam Opt. and Control 98], nous nous plaçons dans le cadre d'une observation partielle du système. Notre solution se fait en 2 étapes: Lors la première, nous dérivons du système partiellement observé un observateur, appelé C-Observer, qui "mémorise" une approximation du coût des trajectoires non-observables. Une notion de coûts observables sur les trajectoires est définie à partir de cette observateur. Durant la seconde étape, nous utilisons l'algorithme présenté dans [Sengupta & lafortune Siam Opt. and Control 98] pour synthétiser une sous machine optimale du C-Observer, correspondant au comportement optimal du système initial.
http://www.irisa.fr/bibli/publi/pi/2000/1359/1359.html
http://www.irisa.fr/prive/hmarchan

Au cours de cet exposé on abordera la testabilité des logiciels OO à deux moments du cycle de dévelopement. On présentera d'abord une évaluation de la robustesse du logiciel basée sur la conception par contrats. Le second aspect, plus prospectif, consistera à réfléchir s'il est possible d'évaluer la testabilité dès la conception à partir du diagramme de classes UML.

On rappellera d'abord les problèmes posés par les jeux sur les graphes finis, et les applications à la vérification (model-checking du mu-calcul). On s'intéresse particulièrement aux jeux à deux joueurs sur les graphes de transitions des automates à pile. Suite aux travaux d'Esparza et autres, on propose une procédure pour déterminer l'ensemble gagnant des jeux d'accessibilité (où l'un des joueurs veut atteindre un ensemble rationnel de configurations). On peut ensuite construire effectivement la stratégie gagnante, ce qui revient à la synthèse de contrôleurs. La suite de ce travail concerne les jeux « à la Büchi ».
http://www-i7.informatik.rwth-aachen.de/~cachat/

We consider the problem of reasoning about message based systems in finite state environments. One notion of a finite state environment that we consider is that of a bounded buffer. In such a situation, the sender gets blocked when the buffer is full. The computations of such systems can be modelled as n-agent Lamport diagrams. We present a linear time temporal logic which is interpreted on such n-agent diagrams. The formulas of the logic specify local properties using standard temporal modalities and a basic communication modality. The satisfiability and model checking problems for this logic are shown to be decidable.

http://www.imsc.ernet.in/~bmeena