Réunion Versydis
17 octobre 2005 - ENS Cachan
Participants: Paul Gastin, David Janin, Olivier Ly, Anca
Muscholl, Nathalie Sznajder, Igor Walukiewicz, Pascal Weil, Marc
Zeitoun, Wieslaw Zielonka
Programme:
- 9h00 - Paul Gastin :
Uniform satisfiability problem
for local temporal logics over Mazurkiewicz traces
(Joint work with Dietrich Kuske)
- 9h40 - David Janin : Raisonner sur les jeux de parités.
Beaucoup de preuve traitant des calculs de points-fixes, de
la logique ou des automates reviennent à démontrer
l'existence de stratégie gagnante dans un jeux de parité
sous l'hypothèse qu'il en existe dans un autre. Nous
présenterons, à travers plusieurs notion de simulation de
jeux, des outils de preuves permettant d'aider à faire cela.
Cela nous conduira à retrouver des règles du calculs des
séquents propositionelles. Le problème de l'existence
d'un éventuel système de preuves complet (en quel sens ?)
sera aussi abordé.
- 10h20 : Pause
- 10h50 - Wieslaw Zielonka :
Au-delà de jeux de
parité.
(travail commun avec Hugo Gimbert)
Y-a-t-il d'autres jeux intéressants à part de jeux de
parité? Je présente quelques propositions.
- 11h30 - Anca Muscholl : On web services composition
(travail commun avec Igor Walukiewicz)
- 12h10 : Déjeuner
- 13h30 - Nathalie Sznajder :
Synthese de controleur pour les
systemes distribues synchrones
La synth\`ese de contr\^oleur consiste, \'etant donn\'e un
syst\`eme partiellement sp\'ecifi\'e, \`a d\'eterminer un programme
dont la synchronisation avec le syst\`eme v\'erifie une
sp\'ecification donn\'ee. Lorsque le syst\`eme est distribu\'e, il
s'agit de construire des programmes locaux, un pour chaque processus
du~syst\`eme. Des r\'esultats standard sur les jeux multi-joueurs \`a
information incompl\`ete impliquent que ce probl\`eme est
ind\'ecidable pour des sp\'ecifications \LTL. Pour des architecures de
communication dans lesquelles les processus sont ordonn\'es de
fa\c{c}on lin\'eaire et pour lesquelles l'information est transmise
entre processus dans un seul sens, il a par contre \'et\'e montr\'e que
le probl\`eme \'etait (non \'el\'ementairement) d\'ecidable pour des
sp\'ecifications $\mu$-calcul. Apr\`es avoir compar\'e diff\'erents
mod\`eles et avoir extrait les points importants des principaux
r\'esultats ant\'erieurs, ce rapport met en \'evidence un crit\`ere de
d\'ecidabilit\'e pour des p\'ecifications plus naturelles que celles
consid\'er\'ees pr\'ec\'edemment. Cette approche fournit des
r\'esultats de d\'ecidabilit\'e pour des architectures ind\'ecidables
dans d'autres mod\`eles.
- 14h10 - Olivier Ly : D0L-systèmes de graphes et d'arbres.
- 14h50 - FIN