Selected publications at LSV

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.

   address = {Berlin, Germany},
   author = {Chatain, {\relax Th}omas and Paulev{\'e}, Lo{\"i}c},
   booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'17)},
   DOI = {10.4230/LIPIcs.CONCUR.2017.18},
   editor = {Meyer, Roland and Nestmann, Uwe},
   month = sep,
   pages = {18:1-18:16},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {Goal-Driven Unfolding of {P}etri Nets},
   url = {},
   volume = {85},
   year = {2017},

About LSV