*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--16h00                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

***  Vendredi 14 Novembre 2008, 14h00-15h00 *************************

Categorical models of nominal computation, and their implementation

Vincenzo Ciancia, University of Pisa

Re'sume'/ Abstract:

The importance of calculi with name generation and name passing has been
widely recognised in computer science, starting from the definition of the
pi-calculus in the late eighties. Applications are not only in the field of
networking and mobile computing, but also in modelling security protocols
(the spi-calculus), service-oriented languages that feature sessions,
object-oriented languages and so on.

Despite the great importance of the subject, it proved very difficult to
reason about programs that feature name allocation: ordinary set theory
gives rise to non-standard notions of equivalence (e.g. side conditions in
the rules for bisimulation). This problem can be solved by employing
categorical models based on presheaf categories, or on nominal sets, as it
was shown by various works in the nineties.

Moreover, it is difficult to implement algorithms that automatically
manipulate the semantics of nominal calculi, such as partition refinement
or model checking, because infinite-state systems are obtained in very
simple cases, even when employing presheaf categories or nominal sets. For
this reason, another categorical model, which is radically different from
presheaf categories, was developed: the model of "named sets", whose
transition systems are called "history dependent automata with symmetries"
and basically allow to reuse old names that will never be used again. This
is obtained by considering names as local, rebindable resources rather than
absolute "constants" whose meaning is globally established, as it happens
in the pi-calculus.

In this talk we will see how the problem of name allocation is solved in a
simple and elegant way from a theoretical point of view by transition
systems (coalgebras) over presheaf categories, and how an equivalence of
categories allows us to automatically translate such models into history
dependent automata that are suitable for verification in many cases.

Also, we will discuss an huge algorithmic benefit of history-dependent
automata, due to the use of symmetries attached to states: the minimal
system obtained by (the categorical notion of) partition refinement has the
least possible number of names and the greatest possible symmetry. This
gives us a procedure to automatically remove redundant names (in the cases
where this problem is decidable) and to find the greatest symmetry group of
the system up-to bisimulation. By representing this group using generators,
a compact description of the system itself is obtained, which can be
exponentially smaller than the original one.


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