过程重写系统和一类基于动作的正则属性的模型检测
摘要：Process Rewrite Systems (PRSs)中的模型检查问题是我们考虑的问题，它是一种无限状态的形式化方法（非图灵强大），可以替代许多常见的模型，如推动过程和Petri网。PRSs可以作为具有动态创建和同步并发进程以及递归过程的程序的形式化模型。PRSs和基于动作的线性时态逻辑（ALTL）的模型检查问题是不可判定的。然而，某些有趣的ALTL片段的可判定性仍然是一个开放问题。在本文中，我们对PRSs中关于无限推导（无限术语重写）的广义接受性属性的可判定性结果进行了陈述。作为结果，我们获得了PRSs和一个有意义的ALTL片段的模型检查（限定为无限运行）的可判定性。
作者：Laura Bozzelli
论文ID：cs/0405003
分类：Other Computer Science
分类简称：cs.OH
提交时间：2007-05-23