Selected publications at LSV

We integrate two compact data structures for representing state spaces of Petri nets: merged processes and contextual prefixes. The resulting data structure, called contextual merged processes (CMP), combines the advantages of the original ones and copes with several important sources of state space explosion: concurrency, sequences of choices, and concurrent read accesses to shared resources. In particular, we demonstrate on a number of benchmarks that CMPs are more compact than either of the original data structures. Moreover, we sketch a polynomial (in the CMP size) encoding into SAT of the model-checking problem for reachability properties.

   address = {Milano, Italy},
   author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Khomenko, Victor},
   booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'13)},
   DOI = {10.1007/978-3-642-38697-8_3},
   editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
   month = jun,
   pages = {29-48},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Contextual Merged Processes},
   url = {},
   volume = {7927},
   year = {2013},

About LSV