Petri网是一种重要的数学模型,它能够有效地对并发系统进行描述和建模。线性时序逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能够方便、准确地描述并发系统的重要性质,如安全性和活性。自动机理论在模型检测中起着非常重要的作用,模型检测是时序逻辑和自动机理论的有机结合,是关于系统性质验证的算法和方法,它通常采用搜索状态空间的方法来检测一个给定的系统模型是否满足某个用时序逻辑公式表示的特定性质。系统模型的状态空间爆炸问题就是模型检测所面临的主要问题。本文详细地描述了Petri网、线性时序逻辑、Büchi自动机、Petri网的可达图和自动机的交自动机,并详细探讨了在基于线性时序逻辑和自动机理论的Petri网的可达图的模型检测策略的基础上,引入了on-the-fly技术来进行Petri网的模型检测。在on-the-fly模型检测中,事先仅需要构造被验证性质对应的自动机和系统的Petri网模型,在对状态空间的搜索中按照双DFS算法的需要动态地构造Petri网的状态可达图和性质自动机的交自动机,与此同时,利用性质自动机来引导Petri网的状态可达图进行动态地构造。这样,在找到被验证性质的一个反例之前,可能仅需要构造交自动机和状态可达图的部分甚至是一小部分的状态空间,从而避免了对交自动机的整个状态空间的穷尽搜索,来尽可能地减少搜索的状态空间,以此来减缓状态空间爆炸的问题。并且存储Petri网模型的可达图以及可达图和性质自动机的交自动机所占用的空间也会减少,从而也可以很好地缓解内存不足的问题。