Reachability Analysis of Process Rewrite Systems
Reachability Analysis of Process Rewrite Systems
复制标题
流程重写系统的可达性分析
DOI：
10.1007/978-3-540-24597-1_7
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Tayssir Touili
中科院分区：
文献类型：
--
作者：
A. Bouajjani;Tayssir Touili
进程重写系统（简称 PRS）包含许多常见（无限状态）模型，例如下推系统和 Petri 网。它们可以被采用作为具有过程调用的并行程序（多线程程序）的正式模型。我们开发了自动机技术，允许构建 PRS 的可达配置的前向/后向集合的有限表示，以各种项结构等价为模（对应于顺序组合和并行组合的运算符的属性）。我们证明，在几种情况下，这些可达性集可以用多项式大小的有限自下而上树自动机来表示。当考虑并行组合的结合性和交换性时，有时需要基于（可判定类）计数器树自动机的非常规表示。
Process Rewrite Systems (PRS for short) subsume many common (infinite-state) models such as pushdown systems and Petri nets. They can be adopted as formal models of parallel programs (multithreaded programs) with procedure calls. We develop automata techniques allowing to build finite representations of the forward/backward sets of reachable configurations of PRSs modulo various term structural equivalences (corresponding to properties of the operators of sequential composition and parallel composition). We show that, in several cases, these reachability sets can be represented by polynomial size finite bottom-up tree-automata. When associativity and commutativity of the parallel composition is taken into account, nonregular representations based on (a decidable class of) counter tree automata are sometimes needed.