Construction and SAT-based verification of Contextual Unfoldings

Stefan Schwoon 1 César Rodríguez 1
1 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 : Unfoldings succinctly represent the set of reachable markings of a Petri net. Here, we shall consider the case of contextual nets, which extend Petri nets with read arcs, and which are more suitable to represent the case of concurrent read access. We discuss the problem of (efficiently) constructing unfoldings of such nets. On the basis of these unfoldings, various verification problems can be encoded as satisfiability problems in propositional logic.
Type de document :
Communication dans un congrès
Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni. Proceedings of the 13th International Workshop on Descriptional Complexity of Formal Systems (DCFS'11), 2011, Limburg, Germany, Germany. Springer, 6808, pp.34-42, 2011, 〈10.1007/978-3-642-22600-7_3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00779945
Contributeur : Stefan Haar <>
Soumis le : mardi 22 janvier 2013 - 17:33:37
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

Citation

Stefan Schwoon, César Rodríguez. Construction and SAT-based verification of Contextual Unfoldings. Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni. Proceedings of the 13th International Workshop on Descriptional Complexity of Formal Systems (DCFS'11), 2011, Limburg, Germany, Germany. Springer, 6808, pp.34-42, 2011, 〈10.1007/978-3-642-22600-7_3〉. 〈hal-00779945〉

Partager

Métriques

Consultations de la notice

151