@INPROCEEDINGS{AB07,
  title = {{Type abstractions of name-passing processes}},
  author = {{Lucia} {Acciai} and {Michele} {Boreale}},
  booktitle = {Proc. of 2nd International Symposium on Foundations of Software Engineering (FSEN'07)},
  pages = {302-317},
  abstract = {We study methods to statically approximate "first-order" process calculi (Pi,
      Join) by "propositional" models (CCS, BPP, Petri nets). We consider both open
      and closed behaviors of processes. In the case of open behavior, we propose a
      type system to associate pi-calculus processes with restriction-free CCS types.
      A process is shown to be in simulation relation with each of its types, hence
      safety properties that hold of the types also hold of the process. We refine
      this approach in the case of closed behavior: in this case, types are BPP
      processes. Sufficient conditions are given under which a minimal BPP type can
      be computed that is bisimilar to a given process. These results are extended to
      the Join calculus using place/transition Petri nets as types.
      },
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {4767},
  year = {2007},
  url = {http://rap.dsi.unifi.it/sensoria/files/FSEN07.pdf},
  invited = {N},
  keywords = {behavioral-types, BPP, join-calculus, Petri nets, pi-calculus},
  partner = {DSIUF, LIF},
}