Approximating Petri Net Reachability Along Context-free Traces

Authors Mohamed Faouzi Atig, Pierre Ganty

Thumbnail PDF


  • Filesize: 0.54 MB
  • 12 pages

Document Identifiers

Author Details

Mohamed Faouzi Atig
Pierre Ganty

Cite AsGet BibTex

Mohamed Faouzi Atig and Pierre Ganty. Approximating Petri Net Reachability Along Context-free Traces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 152-163, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) (with reachability as acceptance condition) is empty. Our contribution to solve this long-standing problem which relates, for instance, to the reachability analysis of recursive programs over unbounded data domain, is to identify a class of CFLs called the finite-index CFLs for which the problem is decidable. The k-index approximation of a CFL can be obtained by discarding all the words that cannot be derived within a budget k on the number of occurrences of non-terminals. A finite-index CFL is thus a CFL which coincides with its k-index approximation for some k. We decide whether the intersection of a finite-index CFL and a PNL is empty by reducing it to the reachability problem of Petri nets with weak inhibitor arcs, a class of systems with infinitely many states for which reachability is known to be decidable. Conversely, we show that the reachability problem for a Petri net with weak inhibitor arcs reduces to the emptiness problem of a finite-index CFL intersected with a PNL.
  • Petri nets
  • Context-free Grammars
  • Reachability Problem


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads