卢委红，丁志军

1.同济大学电子与信息工程学院，上海201804

2.同济大学教育部嵌入式系统与服务计算重点实验室，上海201804

3.同济大学上海市电子交易与信息服务协同创新中心，上海201804

Petri 网是一种重要的形式化建模工具，能有效地对信息系统进行描述和建模.作为一种系统模型，Petri 网不仅可以刻画系统的结构，还可以描述系统的动态行为；既有直观的图形表示，又可以引入许多数学方法分析其性质.Petri 网具有可达性、有界性、活性等[1]重要的性质，同Petri 网所模拟的实际系统联系密切.

在这些性质中，Petri 网的有界性[2]反映了被模拟系统运行过程中对有关资源的容量要求.如果能够求出每个库所p的界b，那么在系统设计时，只要库所p所表示资源的容量不小于b，就能保证系统正常运行.此外，库所界的信息还可以指导可达标识的存储，通过位存储的方式减少存储可达标识所需的空间.也就是说，若已知库所p的界为b，则只需lbb比特的存储空间来存储该库所的标识数.

目前求解库所界的方法有两种：一种方法是完全生成状态空间[2-3]，但对存储空间的要求过高；另一种方法是用P 不变量估计库所界[4]，但存在无法精确求解所有库所界的问题.为此，本文提出了一种基于部分状态空间存储求解库所界的算法，在Petri 网生成状态空间的过程中，只需存储其中一部分能标识就可以精确求解所有库所的界.实验中选取了模型检测竞赛中的部分模型，并对3 种求解界的方法进……