High level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains. However, their strong expressive power hinds their analyzability. In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs - predicate transition (PrT) nets. This method extends and improves our prior results by covering more PrT net features including full first order logic formulas and exploring additional alternative translation schemes. This new analysis method is supported by a tool chain - front end PIPE+ for creating and simulating PrT nets and back end SPIN for model checking safety and liveness properties. We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015. We discuss several properties and show the detailed model checking results of two properties in one system.
