Approximating Petri Net Reachability Along Context-free Traces

TL;DR

This paper introduces a decidable class of context-free languages called finite-index CFLs for which Petri net intersection emptiness can be decided, advancing reachability analysis of recursive programs over unbounded data.

Contribution

It identifies finite-index CFLs as a new decidable class for Petri net intersection emptiness and reduces the problem to Petri nets with weak inhibitor arcs.

Findings

Decidability of intersection emptiness for finite-index CFLs and Petri nets.

Reduction of Petri net reachability with weak inhibitor arcs to CFL intersection emptiness.

Establishment of a correspondence between finite-index CFLs and Petri nets with weak inhibitor arcs.

Abstract

We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) 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.