正规形式下的过程重写系统的验证
摘要：Process Rewrite Systems (PRSs)中模型检查的问题、标准形式下每个重写规则要么只涉及过程调用和过程终止，可能包括返回值（这种规则可以捕获推动过程），要么只涉及过程的动态激活和同步（这种规则可以捕获Petri网络）。PRS和基于动作的线性时态逻辑（ALTL）的模型检查问题是不可判定的。然而，关于PRS和ALTL某些有趣片段的模型检查的可判定性问题仍然是一个未解决的问题。在本文中，我们提出了关于PRS标准形式中无限推导（无限术语重写）的广义接受性质的可判定性结果。作为结果，我们得到了PRS标准形式的模型检查（限于无限运行）和一个有意义的ALTL片段的可判定性。
作者：Laura Bozzelli
论文ID：cs/0401013
分类：Other Computer Science
分类简称：cs.OH
提交时间：2007-05-23