Verification of Scenarios in Petri Nets Using Compact Tokenflows

Issue title: Application and Theory of Petri Nets and Concurrency. PETRI NETS 2013

Article type: Research Article

Authors: Bergenthum, Robin | Lorenz, Robert

Affiliations: Department of Software Engineering and Theory of Programming, FernUniversität in Hagen, Germany. robin.bergenthum@fernuni-hagen.de | Lecturing Professorship for Computer Science, University of Augsburg, Germany. robert.lorenz@informatik.uni-augsburg.de

Note: [] Address for correspondence: Department of Software Engineering and Theory of Programming, FernUniversität in Hagen, Germany

Abstract: In this paper we tackle the problem of verifying whether a scenario is executable in a Petri net. In contrast to sequentially ordered runs, a scenario includes both information about dependencies and independencies of events. Consequently, a scenario allows a precise and intuitive specification of a run of a concurrent or distributed system. In this paper we consider Petri nets with arc weights, 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. We introduce a new compact characterization of the partial language of a Petri net. This characterization is optimized with respect to the verification problem. The paper is a revised and extended version of the conference paper [10].

DOI: 10.3233/FI-2015-1172

Journal: Fundamenta Informaticae, vol. 137, no. 1, pp. 117-142, 2015