Verification of scenarios in Petri nets using compact tokenflows (Q2805422)

A scenario is a specification model that can express causal dependencies and concurrency. In the paper the problem of verifying whether a scenario is executable in a Petri net is studied. Two types of Petri nets with arc weights are studied, namely marked place/transition nets (p/t-nets) and p/t-nets with inhibitor arcs (pti-nets). A scenario of a p/t-net is a labelled partial order (lpo). A scenario of a pti-net is a labelled stratified order structure (lso). Accordingly, the question is either whether a given lpo is in the language of a given p/t-net or whether an lso is in the language of a given pti-net. Different approaches exist to define the partial language of a Petri net. Each definition yields a different verification algorithm, but existing algorithms perform quite poorly in terms of runtime for most examples. A new compact characterization of the partial language of a Petri net is introduced. This characterization is optimized with respect to the verification problem. The paper is a revised and extended version of the conference paper [the first author, Lect. Notes Comput. Sci. 7927, 330--348 (2013; Zbl 1335.68163)].