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], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Communication dans un congrès
Koutny, Maciej and Ulidowski, Irek. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), 2012, Newcastle, United Kingdom. Springer, 7454, pp.471-485, 2012, 〈10.1007/978-3-642-32940-1_33〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776598
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:37:23
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

108