|
|
Seminars for 2004-2005
- Model Checker Aided Design of a Controller for a Wafer Scanner
- Speaker: Frits Vaandrager, Nijmegen Institute for Computing and Information Sciences
- Date: November 12th, 2004
- Abstract:
I intend to present an overview of some recent work that has
has been carried out within the EU IST project AMETIST, in
which timed automata technology is applied to solving various
scheduling problems.
One case study that I will discuss in more detail was
carried out together with Martijn Hendriks (Nijmegen) and
Barend van den Nieuwelaar (ASML/TUE). For a design of a
new wafer scanner for the semiconductor industry, we show
how model checking techniques can be used to compute (i) a simple yet optimal deadlock avoidance policy, and (ii) an infinite schedule that optimizes throughput. Deadlock avoidance is studied based on a simple finite state model using SMV, and for throughput analysis a more detailed timed automaton model has been constructed and analyzed using the UPPAAL tool. The SMV and UPPAAL models are formally related through the notion of a stuttering bisimulation. The results were obtained within two weeks, which confirms once more that model checking techniques may help to improve the design process of realistic, industrial systems. Methodologically, the case study is interesting since two models (and in fact also two model checkers) were used to obtain results that could not have been obtained using only a single model (tool).
- Quelques problèmes dans l'arithmétique de Presburger et l'arithmétique de
Skolem.
- Speaker: Denis Lugiez,
Université de Provence (U1) Marseille (FRANCE)
- Date: March, 4th, 2005
- Venue: Auditorium H, Forum building, Campus Plaine
- Abstract:
L'étude des nombres est un des domaines les plus ancien des mathématiques et a
suscité la curiosité des mathématiciens depuis les temps les plus
reculés. Depuis les travaux des logiciens du siècle précédent on sait qu'il
est vain de vouloir tout connaitre de l'arithmétique dans laquelle on autorise
la multiplication et l'addition. Mais ces logiciens ont aussi montré
rapidement que si on n'utilise que l'addition (arithmétique de Presburger) ou
que la multiplication (arithmétique de Skolem) alors on obtient des théories
décidables. Ensuite l'informatique est arrivée, et on s'est aperçu que ces
théories logiques qui semblaient n'etre que des objets logiques intéressants
mais uniquement théoriques étaient très utiles pour plusieurs applications de
cette discipline, en particulier pour l'étude formelle de systèmes
informatiques ou modelisés par des sytèmes informatiques, domaine en plein
developpement actuellement. On ne compte plus les systèmes de preuve
automatiques ou semi-automatiques qui utilisent une procédure de décision de
l'arithmétique de Presburger (reposant sur l'élimination de quantificateur ou
des méthodes d'automates en général).
Cela relance l'intéret sur l'étude de ces théories et alors que le domaine
semblait bien connu, on s'aperçoit que certains problèmes méritent d'être
repris et que des questions intéressantes restent encore sans réponse
satisfaisante. Le premier sujet que j'aborderai dans cet exposé concerne les
différentes représentations des solutions d'une formule de l'arithmétique de
Presburger. Celles-ci peuvent etre représentées par la formule (après
élimination des quantificateurs par exemple), mais ausi par un ensemble
semi-linéaire ou encore par un automate qui reconnait les représentations
binaires des tuples de solutions. Chaque formalisme a des avantages et des
inconvénients selon les calculs qu'on veut effectuer, et il est donc
intéressant de passer efficacement de l'un à l'autre (si cela est possible).
Le formalisme automate permet de représenter plus d'ensembles et caractériser
les automates qui correspondent à l'arithmétique de Presburger est un résultat
difficile du à Semenov. Muchnik en donne une preuve accessible mais sa
méthode reste encore inutilisable en pratique. Je rappelerai les résultats
obtenus par Latour et Leroux pour le calcul d'une formule à partir d'un
automate et je présenterai les résultats que j'ai obtenus pour passer d'un
automate à la forme semilinéaire pour certains types d'ensembles et des
résultats (ou questions) sur la complexité des représentations. Je terminerai
en donnant quelques indications sur les résultats récents de Leroux pour le
passage automate vers formules.
Ensuite je parlerai du parent pauvre, l'arithmétique de Skolem, en rappelant
rapidement quelques résultats de base sur cette théorie et je montrerai
comment elle peut être utilisée pour prouver des résultats de décidabilité
sur une théorie de multi-ensembles équipée d'opération(s) de comptage.
- Contrôle de systèmes distribués.
- Speaker: Paul Gastin, LSV Cachan (France)
- Date: April, 15th, 2005
- Venue: Auditorium F, Forum building, Campus Plaine
- Abstract:
Dans la panoplie des méthodes formelles utilisées pour assurer la
sécurité des systèmes informatiques, la synthèse de contrôleurs
constitue une approche particulièrement intéressante. Dans ce cadre,
on suppose donnés d'une part un modèle de système ouvert (atelier de
production, ...) dont les actions peuvent être soit contrôlables par
programme soit incontrôlables (environnement) et d'autre part une
spécification décrivant l'ensemble des comportements souhaitables.
L'objectif est de synthétiser, si cela est possible, un contrôleur
agissant uniquement sur les actions contrôlables de telle sorte
qu'indépendamment des actions de l'environnement, les comportements du
système restent corrects. Ce problème a été largement étudié dans le
cadre séquentiel des systèmes à événements discrets depuis les travaux
fondateurs de Ramadge et Wonham. Dans tous les cas raisonnables, on
peut décider si le système est contrôlable et, si oui, synthétiser un
contrôleur. L'intérêt principal de la synthèse de contrôleur est que
l'on obtient des systèmes sûrs par construction, il est donc inutile
de les vérifier ensuite.
La plupart des systèmes complexes aujourd'hui présentent des aspects
distribués. Les processeurs exécutent plusieurs tâches simultanément,
ils coopèrent et communiquent par échange de messages au travers de
réseaux, ils doivent réagir aux stimuli d'un environnement, etc. De
tels systèmes informatiques contrôlent des éléments critiques
(centrales nucléaires, réseau ferré, ...) ou sont embarqués pour
rendre des services cruciaux dans des véhicules, des cartes à puces,
des téléphones, etc. Le problème du contrôle se pose donc très
naturellement dans le cadre des systèmes distribués. La difficulté
supplémentaire est liée au fait que les contrôleurs doivent être
locaux aux composants du système et n'ont qu'une connaissance
partielle des comportements puisqu'ils ne peuvent observer que
localement ce qui se passe sur leur composant.
Les premiers travaux de Pnueli et Rosner sur le contrôle distribué
étaient motivés par la synthèse de programmes pour les circuits. Ils
ont naturellement considéré des systèmes totalement synchrones et ont
montré que même pour des spécifications simples (LTL) le problème du
contrôle est indécidable pour presque toutes les architectures de
circuits. Les architectures décidables sont essentiellement de type
"pipeline". Ces résultats ont été généralisés par Kupferman et Vardi
pour des spécifications CTL^* et pour le mu-calcul et par Madhusudan
et Thiagarajan pour des spécifications locales.
Les problèmes de contrôle sont souvent décrits et résolus en utilisant
des jeux dans lesquels un joueur représente le contrôleur et son
adversaire est l'environnement. Dans le cadre distribué, on considère
plusieurs joueurs (les contrôleurs locaux) et un environnement. Il
s'agit de jeux à information partielle puisqu'à nouveau la stratégie
d'un joueur ne doit dépendre que de ce qu'il a pu observer localement.
Mohalik et Walukiewicz ont utilisé cette approche dans le cadre du
contrôle distribué, obtenant grâce à deux techniques de réduction tous
les cas décidables précédents.
Avec Lerman et Zeitoun, j'ai reconsidéré le problème du contrôle
distribué en changeant quelques hypothèses. D'une part, nous nous
plaçons dans un cadre asynchrone et nous considérons des
spécifications correspondant à des reconnaissables de traces de
Mazurkiewicz. D'autre part, nous autorisons les contrôleurs à utiliser
une mémoire causale plutôt qu'une mémoire purement locale. Cette
mémoire causale, qui permet à un joueur de baser sa stratégie sur tout
son passé causal, peut être implantée sur l'architecture considérée
simplement en surchargeant les messages échangés dans l'exécution
normale du système. Nous avons montré que sous ces hypothèses, le
problème du contrôle distribué est décidable pour toutes les
architectures série-parallèles et toutes les spécifications
reconnaissables. Ce résultat positif contraste fortement avec les
résultats essentiellement négatifs précédents.
- Decidable and undecidable problems in decentralized observation and control
- Speaker: Stavros Tripakis (CNRS, Verimag)
- Date: May, 20th, 2005
- Abstract:
The problems of checking existence of and synthesizing (when they exist)
observers and controllers are essentially closed in the centralized
case, that is, the case of a single observer/controller for the entire
plant. The situation is much less clear in the decentralized case. One
thing is certain, however: undecidability is common in decentralized
settings.
In this talk I will try to give an overview of what I believe are key
facts in decentralized observation and control. I will present both
decidable and undecidable problems (including old results such as
[Pnueli-Rosner 1991], and newer results in the discrete-event system
framework) in an attempt to identify the limits of (un)decidability.
Follow these links to access the lists of 2002-2003
and 2003-2004 seminars.
Links to other seminars
|
|