Petri网是一种广泛应用于描述异步并发现象的图形化建模和分析工具，Petri网的可达性判定问题是进行Petri网建模和分析的基础。判定Petri网可达性的基本方法有可达树、可达图、状态方程和不变量分析等，由于合爆炸问题的存在，使得这些基本Petri网的分析方法随着问题规模的增大而超出目前计算机的运算能力，严重限制着Petri网建模机制在现实中的应用。本文采用逻辑抽象技术和约束程序的方法，主要对三种类型的可达问题进行的研究。即：问题1：给定Petri网∑=（P，T；F，W，m₀）和任一标识m_f，判断该标识是否由初始标识m₀可达。问题2：给定Petri网∑=（P，T；F，W，m₀）和一组标识，求这组标识中的元素从初始标识m₀可达的情况。问题3：给定Petri网∑=（P，T；F，W，m₀）和任一T_向量U，判断是否有对应T_向量U的实际变迁序列由初始标识m₀发生。即在对应T_向量U的实际变迁序列的作用下标识m_f=m₀+C.U是由初始标识m₀可达。针对以上3个问题，本文具体工作为：首先，在分析逻辑抽象技术和序列深度参数算法的基础上，引入最大步集、部分标识的关键标识、部分步关键变迁等概念，证明关键约束的可用、完整和正确性。丰富了基于约束程序的Petri网理论。其次，提出了解决问题1、问题2的基于关键约束理论的可达集及序列深度参数求解算法和可达判定算法。使得算法不但可以在并行度高、多Token或存在家态情况下，使用更少约束和变量，避免搜索重复路径与产生重复标识；而且对有界Petri网判定时，不需要指定K值，并可以一次对一组标识完成可达判定。大大地提高了判定的效率和适用范围。最后，在分析变迁约束可达问题的各种求解办法和缺陷的基础上，提出了变迁约束可达问题的求解模型和判定算法。使用该约束模型的构造的算法充分利用T_向量提供的信息，对可达图进行展望搜索，忽略了对不相关分支的搜索；在约束搜索策略的指导下，使得变量（解）快速逼近于T_向量。通过实例分析表明，算法在多Token、多并发、大最大步集的情况下，将大大减少了问题搜索的分支。最坏情况下（在不可达并且单Token的情况下）算法才有可能等同于关键约束的搜索量。另外，问题搜索所减少搜索的分支的数量和网结构及其token数有关。