[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Frits asked me to forward this on moca (he does not subscribe and thus cannot post himself)

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

--- Begin Message --- 
Dear Joachim,

Nice to hear from you again!

I did some work on decidability for process algebras which appeared as

F.W. Vaandrager. Expressiveness results for process algebras. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Semantics: Foundations and Applications. LNCS 666, pages 609-638. Springer-Verlag, 1993. Available as CWI technical report CS-R9301.

In my paper, though, I mainly restricted attention to guarded recursion. In the presence of unguarded recursion, you get infinite branching
and different notions of decidability are needed: one may consider
for which languages the transition relation is r.e. or one
may consider decidability of the question "is there an a-transition
from expression P to expression Q". In my paper I refer to Boudol's
paper "Notes on Algebraic Calculi of processes" from 1985, who
claims that in the presence of unguarded recursion it is even
undecidable whether a MEIJE/SCCS expression has an outgoing
transition at all. I don't have the paper at hand so I don't
know if/how Boudol proves this. But it is not hard to see that
Boudol's claim is correct. Recall that in MEIJE/SCCS one can
specify any operator in the De Simone format. Thus, in particular,
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).
Now with unguarded recursion one can specify

	Xn = (q0,t0,u0) . NIL + next_n (Xn)

Here (q0,t0,u0) is the initial configuration of the n-th Turing
machine.  Process Xn  has infinite branching and spits out all
configurations of the n-th Turing machine.
Now the restriction of Xn in which only halting configuration
actions are permitted has an outgoing transition iff the n-th
Turing machine halts.

Regards,

Frits


Dear Moca, and Frits (who may have done related work but may not be on Moca),

Has it been determined exactly under what circumstances it is decidable what transitions an agent has? In "Bisimulation can't be traced" (POPL 1988) Bloom, Istrail and Meyer make a remark that in the presence of unguarded recursion this is undecidable and I believe this is kind of folklore, but I have not actually seen a proof or a closer investigation.

A related question is decidability of structural congruence - is this problem still open?

Joachim Parrow

.



--
My new email address is : F.Vaandrager@xxxxxxxxx
The University of Nijmegen has changed its name to Radboud University Nijmegen.


--- End Message ---