Petri网具有严格的数学基础和直观的图形化表示，一直是离散事件系统建模分析、控制与仿真的主要工具之一。然而，Petri网的理论方法中的无界网可达性分析问题一直是困扰着各国学者的世界性难点问题。针对这一问题，本文提出了一种精准有限可达树(Exact Finite Reachability Tree，EFRT)，并用于可达性分析理论方法的研究。具体工作与成果如下:　　(1)首次深入分析了无界网无界库所的产生机理与根源，以及状态可达性的本质，给出了无界库所判定的一个充分非必要条件，突破了人们对无界网可达性问题的认识局限。　　(2)提出了一种全新的EFRT，结合新提出的“充分使能”条件确保了该树对广义无界网可达状态的完全表征。EFRT的ω节点只能作为叶节点存在且不再生长，每个这样的标识只包含一个ω量，突破了现有的有限可达树的ω节点参与生长且标识表达式复杂等局限。同时，EFRT允许ω节点以最小普通标识来继续展开，这为后续的基于树搜索的增量式可达性分析打开了方便之门。　　(3)基于EFRT建立了无界网可达性分析理论方法，给出了包括可达性、有界性、安全性、死锁、活性、可逆性等属性的分析理论与算法，对所有理论结论都进行了严格证明。突破了现有的可达性理论多集中于死锁分析的现状。　　(4)依据上述的理论结果和算法，设计开发了基于EFRT的无界Petri网属性分析软件，实现了EFRT的生成，以及有界性、安全性、死锁、活性、可逆性等属性的分析。最后用实例验证了本文提出的理论和方法。　　综上，提出的EFRT适应于广义无界Petri网的状态表示，并且建立的可达性分析理论方法是有效。本文的理论方法将有望进一步推广到无界网一般可达性的分析中。