Selected publications at LSV

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.

   address = {Limburg, Germany},
   author = {Schwoon, Stefan and Rodr{\'\i}guez, C{\'e}sar},
   booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop on {D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'11)},
   DOI = {10.1007/978-3-642-22600-7_3},
   editor = {Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni},
   month = jul,
   pages = {34-42},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Construction and {SAT}-based verification of Contextual Unfoldings},
   url = {},
   volume = {6808},
   year = {2011},

About LSV