Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings

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].

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Claus Schröter, Victor Khomenko
• Keywords: CAV 2004, Formal Methods, Low-level Nets, LTL-X Modelchecking, Unfolding-based Approach