On Decidability of the Control Reachability Problem in the Asynchronous pi-Calculus
On Decidability of the Control Reachability Problem in the Asynchronous pi-Calculus
复制标题
异步π微积分中控制可达问题的可判定性
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Charles Meyssonnier
中科院分区：
文献类型：
--
作者：
R. Amadio;Charles Meyssonnier
我们研究了异步π演算的各个片段的控制可达性问题的可判定性。我们考虑三个主要特征的组合：名称生成，名称移动性和无界控制。我们表明，名称生成与名称移动性或无界控制的组合导致一个不可判定的片段。另一方面，我们证明了唯一的接收器和有界输入（一个条件弱于有界控制）的名称生成是可判定的转移（和回）的Petri网的覆盖性问题的减少。
We study the decidability of the control reachability problem for various fragments of the asynchronous π-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation with unique receiver and bounded input (a condition weaker than bounded control) is decidable by reduction to the coverability problem for Petri nets with transfer (and back).