structural congruence

["Gelsema, drs. T.E." <TGSA@xxxxxx>]

Hello all,

Joost and I constructed a model for a version of SC that differs from
the SC of Milner's "Functions as Processes" only in the substitution of

!(P | Q) == !(P | Q) | P

for the ususal law for replication (the original law is implied by this new
one).
Using a transformation of processes we reduced the decidability of this new
congruence to the decidability of the extended congruence (the latter is the
one with, among others, the distributivity law of replication over
composition;
see TCS 211). This result is written down in a preliminary paper called
"Potential
Congruence of the pi-Calculus with Replication" (Unfortunately, I don't have
this
at hand at the moment; anyone interested can download it from my homepage
in Leiden).

Also, we proved decidability of a version of SC that only excludes the law

(nu x)(P | Q) == (nu x)P | Q, whenever x not free in Q

as well as for full SC with a `limited capacity' (sorry for this) for
replication.

Now I did not have the time to really look into the question posed by Luis,
but I frequently encountered similar questions solving the decidabilities
described above.

Best regards,
Tjalling Gelsema
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html