[moca] completeness of bisimulations for spi-calculus?

[Eijiro Sumii <eijiro_sumii@xxxxxxxxxx>]

Dear all,

I have a question about completeness of bisimulations for
spi-calculus.

It seems that hedged bisimilarity [Borgstrom-Nestmann-02] is supposed
to be complete with respect to barbed equivalence(*1), because hedged
bisimilarity coincides with another complete bisimilarity
[Boreale-DeNicola-Pugliese-99].  However, it also seems that the
latter bisimilarity is proved to be complete for "structurally image
finite" (i.e., image finite modulo structural equivalence) processes
only.  Is there some unpublished result for the general case, or is it
still an open problem?  If so, why is it so difficult?  In particular,
is it hard to prove something like

  S  =  { (P, Q, H) |
          P  \equiv  P' | [M_1,...,M_n/x_1,...,x_n]R,
          Q  \equiv  Q' | [N_1,...,N_n/x_1,...,x_n]R,
          P' and Q' are barbed equivalent,
          H |- M_i <-> N_i for every i = 1, ..., n,
          fn(R) are distinct from fn(H) }

to be a hedged bisimulation or whatever?

(*1) where processes P and Q are barbed equivalent iff P|R and Q|R are
barbed bisimilar for every R, though there seems to be difference of
terminology in some papers

@InProceedings{Borgstrom-Nestmann-02,
  author = 	 {Johannes Borgstr{\"{o}}m and Uwe Nestmann},
  title = 	 {On Bisimulations for the Spi Calculus},
  booktitle = 	 {9th International Conference on Algebraic Methodology and Software Technology},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {287--303},
  year =	 {2002},
  OPTeditor = 	 {},
  volume =	 {2422},
  OPTnumber = 	 {},
  series =	 LNCS,
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 SV,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{Boreale-DeNicola-Pugliese-99,
  author = 	 {Michele Boreale and Rocco {De Nicola} and Rosario Pugliese},
  title = 	 {Proof Techniques for Cryptographic Processes},
  journal = 	 {SIAM Journal on Computing},
  year = 	 {2002},
  OPTkey = 	 {},
  volume =	 {31},
  number =	 {3},
  pages =	 {947--986},
  OPTmonth = 	 {},
  note =	 {Preliminary version appeared in
                  {\emph{14th Annual IEEE Symposium on
                  Logic in Computer Science}}, pp.~157--166, 1999},
  OPTannote = 	 {}
}

Sincerely,

--
Eijiro Sumii (http://www.cis.upenn.edu/~sumii/)
Department of Computer and Information Science, University of Pennsylvania
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html