********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 5 decembre 1997 **** 14h00 ***************************** Temps-reel: logiques, automates et theories classiques Jean-Francois Raskin (FUNDP Namur & LIENS) Re'sume' : La theorie des langages reguliers et omega-reguliers est utile dans l'approche de beaucoup de problemes d'informatique fondamentale. Les relations entre les formalismes pour decrirent ces langages ont ete etudiees en profondeur et sont maintenant bien connues. Par exemple, la logique temporelle lineaire (LTL) a un pouvoir d'expression equivalent au fragment premier ordre de S1S et les automates de Buchi sont strictement plus expressifs et correspondent a S1S. La theorie des langages temporises (temps-reel), ou la notion de distance entre evenements est prise en compte, est une extension de la theorie des langages reguliers. Les premiers travaux sur ces extensions datent du debut des annees 90 et sont bases sur le formalisme des "Timed automata" (Alur et Dill). Malheureusement, ce formalisme n'est pas ferme au complement lorsque l'on modelise le temps avec un domaine dense (les reels par exemple). De plus, les differences d'expressivite entre les formalismes deja definis ne sont pas encore bien comprises. Pour repondre a ces problemes et questions, nous proposons un nouvel ensemble de formalismes (logiques-automates-theories classiques) qui sont tous decidables et fermes au complement. L'expressivite de chacun des formalismes est etudiee et comparee aux autres. On obtient alors une hierarchie de formalismes comme dans le cas non temps-reel. Ce travail est issu d'une cooperation avec Tom Henzinger de l'Universite de Californie a Berkeley et Pierre-Yves Schobbens de l'Universite de Namur. *** Vendredi 12 decembre 1997 **** 14h00 **************************** 1) Rel^ache (AMAST'97) 2) Jubile' M. Nivat, Salle Dussane, ENS. Programme : Vendredi 12 decembre; 16:00 A. Arnold : Accueil et introduction. 16:30 B. Courcelle : Arbres, langages et schemas de programmes. 17:00 A. Podelski : Les automates d'arbres dans l'analyse des programmes 17:30 P.L. Curien : Des combinateurs categoriques aux substitutions explicites. 18:00 Le verre de l'amitie Samedi 13 Decembre; 9:00 B. Rozoy : Modeles du parallelisme. 9:30 M. Dauchet : Mais c'est un bimorphisme ! 10:15 Pause 10:45 G. Senizergues : L(A)=L(B) ? 11:30 G. Cousineau : Programmation fonctionnelle et geometrie. 12:00 14:00 G. Ruggiu et F. Boussinot: Semantique des systemes temps-reels 14:30 P. Aigrain : L'informatique et ses milieux associes 15:00 Pause 15:15 L. Kott : L'informatique theorique : retour vers le futur. 15:45 G. Roucairol : Quelle informatique fondamentale pour l'industrie ? 16:15 Fin *** Vendredi 19 decembre 1997 **** 14h00 **************************** Rel^ache (AMAST'97) *** Vendredi 26 decembre 1997 **** 14h00 **************************** Bonnes Fe^tes. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html *********************************************************************