Petri网是集图形化表示和数学理论于一体的建模语言，可以描述常见的顺序、选择、循环和并行等行为，广泛应用于并发分布式系统的建模、分析和验证。Petri网的语义可以划分为行为语义和状态语义，前者关注执行变迁形成的行为序列，而后者则关注由执行变迁所引发的可达标识序列。进一步，状态语义可以取出不同子集分别形成交织语义、并发语义和极大并发语义。　　为了验证Petri网中繁多且复杂的时序性质，目前已存在多种针对Petri网的模型检测方法。这些方法通常使用线性时序逻辑(Linear Temporal Logic,LTL)和计算树逻辑(Computation Tree Logic,CTL)作为性质描述语言。虽然LTL和CTL具有较强的表达能力，但是未达到完全正则，难以描述Petri网中一些重要且常见的时序性质，例如周期性质。命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)不仅具备完全正则表达能力，而且擅长描述涉及区间、周期和并发的时序性质。此外，现有的Petri网模型检测方法通常只关注一种状态语义，即交织语义。为了充分地验证Petri网的完全正则性质，本文针对上述各种语义研究了Petri网的PPTL模型检测方法。　　为了验证Petri网的交织语义、并发语义和极大并发语义是否满足由PPTL公式描述的性质，本文提出了三种由Petri网到建模仿真验证语言(Modeling,Simulation, and Verification Language,MSVL)程序的集中式转换方法，每种转换方法由Petri网的一种状态语义引导。基于MSVL的操作语义，本文针对每种转换方法证明了Petri网和生成的MSVL程序之间存在一种等价关系。开发了工具PN4MSVL，支持上述三种集中式转换方法。从而可以使用MSVL的现有支持工具MSV对Petri网进行仿真执行、状态空间构造和PPTL性质验证。　　为了验证Petri网的行为语义是否满足PPTL公式描述的性质，基于PPTL的带标记范式图(Labeled NormalForm Graph,LNFG)的构造算法，本文提出了PPTL的on-the-fly模型检测算法。通过交织构造性质的非的LNFG和Petri网的并发可达图(Concurrent Reachability Graph,CRG)，使其相互制约并引导各自节点和边的生成，该算法直接构造两者的乘积图，并同时在该乘积图中寻找与反例对应的成功路径，一旦找到则停止构造。这样避免生成LNFG、CRG和乘积图的完整状态空间。此外，为了进一步应对该模型检测算法的状态空间爆炸问题，本文提出了一组结构化简规则。这些规则可以在不改变Petri网的PPTL性质的前提下化简Petri网的规模，从而削减其状态空间。实现了工具PPTL4PN，支持该模型检测算法和化简规则。　　工作流网(Workflow Nets,WFNs)作为Petri网的经典子集，成功应用于工作流过程的建模。为了按照WFNs迅速并准确地生成程序原型，本文提出了WFNs到MSVL程序的结构化转换方法。该方法首先通过给WFNs的每个变迁添加条件注释和语句注释得到带注释的工作流网(Annotated WFNs,AWFNs)，然后利用一组转换规则不断压缩AWFNs的规则结构直至其只包含一个变迁，最后由该变迁的语句注释构造生成MSVL程序。开发了工具PN2MSVL，支持该结构化转换方法。实验表明PN2MSVL可以将结构较为规则的WFNs转换成具有高可读性的MSVL程序。