Reference: C. Schröter and V. Khomenko. Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. In R. Alur and D. A. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 109–121. Springer-Verlag, 2004. Abstract: We present an unfolding-based approach to LTL-X model-checking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets (EH-00,EH-01) and a state of the art parallel high-level net unfolder described in (KK-03-TACAS,K-03-thesis). We present experimental results comparing our approach to the one of (EH-00,EH-01) and the model-checker Spin (H-03). Suggested BibTeX entry: @inproceedings{SK04,     author = {C. Schr{\"o}ter and V. Khomenko},     booktitle = {Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)},     editor = {R. Alur and D. A. Peled},     pages = {109--121},     publisher = {Springer-Verlag},     series = {Lecture Notes in Computer Science},     title = {{Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings}},     volume = {3114},     year = {2004} }

GZipped PostScript (190 kB)