Faster verification of partially ordered runs in Petri nets using compact tokenflows

Abstract

In this paper we tackle the problem of verifying whether a labeled partial order (LPO) is executable in a Petri net. In contrast to sequentially ordered runs an LPO includes both, information about dependencies and independencies of events. Consequently an LPO allows a precise and intuitive specification of the behavior of a concurrent or distributed system. In this paper we consider Petri nets with arc weights, namely marked place/transition-nets (p/t-nets). Accordingly the question is whether a given LPO is an execution of a given p/t-net. Different approaches exist to define the partial language (i.e. the set of executions) of a p/t-net. Each definition yields a different verification algorithm, but in terms of runtime all these algorithms perform quite poorly for most examples. In this paper a new compact characterization of the partial language of a p/t-net will be introduced, optimized with respect to the verification problem. The goal is to develop an algorithm to efficiently decide the verification problem. © 2013 Springer-Verlag.