论文部分内容阅读
参数化系统（paramterized system）是指包含特定有限状态进程多个实例的并发系统，其中的参数是指系统内进程实例的数目，即系统的规模反向可达性分析（backward reachability analysis）已被广泛用于验证参数化系统是否满足以向上封闭（upward-closed）集合表示的安全性（safety property）与有限状态系统验证相类似，参数化系统的验证同样也面临着状态爆炸（state explosion）问题，并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状态集