Re: [moca] [Fwd: Re: Decidability of semantics]

[Michael Baldamus <michaelb@xxxxxxxx>]

The undecidability theorem stated by Frits seems to refer to a
calculus with an infinite number of channels. What about settings
where the number of channels is (a) finite or (b) infinite where, at
the same time, the channels do not carry any internal structure that
can be referred to by SOS clauses? It seems to me that setting (b)
would apply to the pi-calculus.

To be more specific, Frits wrote:

> one can specify an operator with rules
>
>        P --(q,t,u)--> P'
>        -------------------------
>        -------------------------
>        next_n (P) --(q',t',u') --> P'
>
> such that if (q,t,u) represents a configuration of the n-th
> Turing machine with state q, and tape <t,u>, then (q',t',u')
> represents the configuration obtained by doing a single step
> from (q,t,u)

If this rule is in fact a rule scheme then we end up with infinitely
many actual rules. Then again, if we do admit infinite rule sets, then
the undecidability might be a different question than if we only admit
finite rule sets.

If the rule is not a scheme, then it seems to involve looking inside
the channels to take their internal structure into account. If I am
not mistaken, there is no such thing in pi-calculus SOS clauses.
The only exception might be that names can be tested for equality
or inequality. I wonder whether all of that together might render the
transition semantics of pi decidable even in the presence of unguarded
recursion.

Greetings

  Michael

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