Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00779945
Contributor : Stefan Haar <>
Submitted on : Tuesday, January 22, 2013 - 5:33:37 PM
Last modification on : Monday, February 15, 2021 - 10:48:55 AM

Links full text

Identifiers

Citation

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

Share

Metrics

Record views

213