并发可折叠推入系统的饱和

摘要:多重堆栈推进系统是使用具有一阶过程调用的线程的并发计算的良好研究模型。尽管一般来说,可达性是不可判定的,但对堆栈行为存在许多限制,可以导致可判定性。为了建模高阶过程调用,需要推进栈的一种推广,称为可折叠推进栈。对于多堆栈可折叠推进系统的可达性问题研究很少。在这里,我们使用饱和技术研究有序、相位有界和作用域有界的多堆栈可折叠推进系统,展示了控制状态可达性的可判定性,并给出了可以达到给定控制状态的所有配置的正则表示。

作者:Matthew Hague

论文ID:1310.2631

分类:Formal Languages and Automata Theory

分类简称:cs.FL

提交时间:2013-10-11

PDF 下载: 英文版 中文版pdf翻译中