*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h--16h                         *
*                 Salle W, 4e`me e'tage, toits du DMI               *
*                 DMI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 3 juin 1994 ********************************************

Abstractions for preserving all CTL* formulae

Purushothaman IYER (N.C.  State Univ./ENS Cachan)

Re'sume' : We develop a method for generating abstractions of 
transition systems in a way that preserves properties of the original
system expressible in the temporal logic CTL*.  The technique extends
those developed for fragments of this logic by Dams, Grumberg and Gerth
and behaves at least as well as the democratic abstractions they 
introduce for the whole logic. A small example illustrates the 
application of our approach to the analysis of systems of concurrent
processes.

*** Vendredi 10 juin 1994 *******************************************

Programmer ses propres objets dans le langage ML-ART

Didier REMY (INRIA Rocquencourt)

Re'sume' : Les objets structure's par des classes peuvent se programmer
directement et efficacement dans une extension tre`s simple du langage
ML. La repre'sentation des objets s'appuie sur des types existentiels
et des types enregistrements. Les classes peuvent e^tre structure'es
avec de l'he'ritage multiple, et les objets peuvent se transmettre des
messages de leur propre classe aussi bien que de leurs classes parentes.
Toutefois, il n'est pas possible de coercer un objet avec d'autres objets
lui correspondant dans une classe parente.

Le langage ML-ART est une extension de ML avec des enregistrements
extensibles et des types re'cursifs, existentiels et universels. Dans 
cet expose', nous montrerons essentiellement comment programmer ses 
propres objets dans le langage ML-ART, en introduisant les nouvelles
fonctionnalite's du langage de fac,on informelle. Si le temps, le permet
nous de'crirons le langage ML-ART plus formellement et e'noncerons la
correction du typage pour une se'mantique ope'rationnelle par re'duction.

*** Vendredi 17 juin 1994 ********************************************

Dualit\'e entre r\'eseaux et automates

Eric BADOUEL (IRISA Rennes)

Re'sume' : Le probl\`eme de la {\em synth\`ese de r\'eseaux} est le 
suivant: \'etant donn\'e une famille de r\'eseaux (r\'eseaux de P\'etri, 
r\'eseaux \'el\'ementaire, r\'eseaux trace ...) et un automate (fini), 
on veut pouvoir d\'ecider si cet automate est le graphe de marquage d'un 
r\'eseau de cette famille, en ``synth\'etisant'' un tel r\'eseau \`a partir 
de l'automate.

La solution passe par l'observation suivante: une place d'un r\'eseau est 
une propri\'et\'e locale d'un \'etat, on peut donc assimiler un \'etat \`a 
l'ensemble de ses propri\'et\'es (un marquage est un {\em ensemble} de 
places) mais de fa\c{c}on duale on doit pouvoir assimiler une place \`a 
l'ensemble des \'etats (marquages) qui v\'erifie cette propri\'et\'e. Ceci 
am\`ene a \'etudier les propri\'et\'es structurelles des extensions des 
places d'un r\'eseau dans le graphe de marquage de celui-ci. On aboutit 
ainsi a la notion de {em r\'egion} introduite par Ehrenfeucht et Rozenberg 
dans le cas des r\'eseaux \'el\'ementaires et dont diverses variantes 
existent pour d'autres classes de r\'eseaux.

On indiquera comment de telles correspondances peuvent ^etre d\'ecrites 
comme des dualit\'es concr\`etes dues \`a l'existence d'objets 
schizophr\'eniques entre les cat\'egories correspondances. Ceci nous permet 
\`a la fois de comparer ces diff\'erentes classes de r\'eseaux et d'en 
d\'ecouvrir des extensions naturelles.

*** Vendredi 24 juin 1994 ********************************************

An Old-fashioned Recipe for Real Time

Leslie LAMPORT (DEC-SRC, Palo Alto)

Re'sume' : Real-time systems are a current fad in the world of 
verification and semantics. They provide a wonderful opportunity for 
theoreticians to invent new semantics.  However, it has been known for 
at least a dozen years that there is a straightforward approach for 
applying standard methods to real-time systems.  When combined with TLA 
(the Temporal Logic of Actions), this approach allows the separate 
specification of temporal and nontemporal aspects of a system.  The more 
recent concept of machine closure, introduced four years ago, provides a 
general approach to the problem of ``Zeno'' specifications---ones 
requiring an infinite number of actions to occur in a finite length of 
time.

*********************************************************************