基于Petri网的模型检测研究

模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景