可编程逻辑控制器(PLC)广泛地应用于柔性制造、轨道交通等安全苛求系统,这对PLC程序的正确性和可靠性有严格的要求。由于梯形图是PLC使用最广泛的编程语言,梯形图程序验证研究获得了广泛的关注。虽然梯形图的语法错误可以通过编译器检测出来,但是对于一些隐藏在程序内的逻辑错误(特别是梯形图的竞态),编译器将无能为力。本文主要研究梯形图程序的竞态检测方法,包括两个主要的内容,分别是关系图的竞态检测方法和抑制弧Petri网的竞态检测方法。在基于关系图的竞态检测方法中,首先提出了关系图的概念,并给出梯形图到关系图的转化方法,关系图描述的逻辑关系可以一一对应到梯形图的逻辑关系,发现了关系图的环形结构与可编程逻辑控制器的竞态之间的必然关系并据此给出了梯形图无竞态的一种多项式级计算复杂性的判据。在基于抑制弧Petri网的竞态检测方法中,使用抑制弧Petri网为梯形图建模。并且考虑了PLC循环扫描的工作原理,为抑制弧Petri网添加了顺序控制库所。针对带顺序的抑制弧Petri网,提出了改进的可达图生成算法,通过可达图的结构判断梯形图是否存在竞态。由于初始标识的不同,经常地,会产生多个不同的可达图。当所有的可达图结构都不存在环结构,则该可判断相应的梯形图不存在竞态。本文还给出多个例子,用来验证结论的正确性。