Abstract. We present an unfolding-based approach to LTL-X modelchecking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets [4, 5] and a state of the art parallel high-level net unfolder described in [15, 13]. We present experimental results comparing our approach to the one of [4, 5] and the model-checker Spin [12].