Skip to Main content Skip to Navigation
Conference papers

Verification of Petri Nets with Read Arcs

César Rodríguez 1, 2 Stefan Schwoon 1, 2
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Recent work studied the unfolding construction for contextual nets, i.e. nets with read arcs. Such unfoldings are more concise and can usually be constructed more efficiently than for Petri nets. However, concrete verification algorithms exploiting these advantages were lacking so far. We address this question and propose SAT-based verification algorithms for deadlock and reachability of contextual nets. Moreover, we study optimizations of the SAT encoding and report on experiments.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00776598
Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 15, 2013 - 5:37:23 PM
Last modification on : Monday, February 15, 2021 - 10:50:10 AM

Links full text

Identifiers

Citation

César Rodríguez, Stefan Schwoon. Verification of Petri Nets with Read Arcs. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), 2012, Newcastle, United Kingdom. pp.471-485, ⟨10.1007/978-3-642-32940-1_33⟩. ⟨hal-00776598⟩

Share

Metrics

Record views

184