*********************************************************************
*                       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 7 fe'vrier 1997 **** 14h00 *****************************

Enhanced Operational Semantics for Concurrency

Corrado PRIAMI (Universita di Pisa & ENS)

Re'sume': We extend the classical structural operational semantics to
implement the possibility of having different views of the same system
that are all consistent to one another and that can be recovered
mechanically from a single, concrete representation.
We apply this idea to concurrent and distributed systems, and especially
to mobile agents.

Our concrete representation is a transition system (called
proved and defined in {\em SOS} style),
whose transitions are labelled by encodings of their deduction
trees. The labels of transitions allow us to retrieve all the
main semantic models presented in the literature
and also to define new semantics (e.g. a new causality). These
semantics are retrieved from the proved transition system
through relabelling functions that only maintain
the relevant information in the labels of transitions.

To automate the above approach for verification of distributed
systems, we study the state explosion problem. We overcome it for
languages that do not contain scope operators like {\em CCS}
restriction. Under this assumption we obtain a compact proved transition
system that is linear (in average) with the occurrences of actions in a
process and that preserves non interleaving bisimulation-based
equivalences.

*** Vendredi 14 fe'vrier 1997 **** 14h00 ****************************

Pas de seminaire (groupe de travail).

*** Vendredi 21 fe'vrier 1997 **** 14h00 ****************************

Rela^che.

*** Vendredi 28 fe'vrier 1997 **** 14h00 ****************************

Une methode de tableaux pour la logique du temps lineaire (1ere
partie)

Jean GOUBAULT (Dyade)

Re'sume' : La logique propositionnelle du temps lineaire (LTL) de Manna,
Pnueli et d'autres est un outil raisonnablement puissant de
specification de systemes paralleles.  Il a ete systematiquement sous-utilise,
sans doute par manque de methodes de preuve automatique, et en
particulier de methodes efficaces, notamment si l'on effectue une
comparaison avec les methodes fondees sur le model-checking.  Je ferai
un etat de l'art des methodes et des resultats de complexite
connus sur cette logique, et je vous montrerai un systeme tres
simple de tableaux que j'ai developpe avec Peter Schmitt pendant
mon sejour a Karlsruhe de 1996.  J'essaierai ensuite de vous
convaincre qu'il fournit une methode en general plus efficace que toutes
les techniques connues precedemment, et que les preuves que la
methode fournit sont, de plus, tres lisibles --- un avantage que
de plus en plus de clients demandent.

Travail commun avec Peter H. Schmitt. 

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr
WWW: http://www.ens.fr/~cousot/annonceseminaire.html
*********************************************************************