Computation of Transition Adjacency Relations Based on Complete Prefix Unfolding (Technical Report)

TL;DR

This paper introduces an efficient method for deriving Transition Adjacency Relations (TAR) from Petri net models using Complete Prefix Unfolding, addressing state explosion issues and validated by experiments on industrial and synthetic models.

Contribution

It formally establishes the equivalence between TAR and Event Adjacency Relation (EAR) in CPU, and provides a verified algorithm with structural boosting rules for TAR computation.

Findings

CPU-based TAR computation scales well with model size and concurrency.

The method effectively alleviates state explosion in concurrent process models.

Formal proofs confirm correctness and generality of the approach.

Abstract

An increasing number of works have devoted to the application of Transition Adjacency Relation (TAR) as a means to capture behavioral features of business process models. In this paper, we systematically study the efficient TAR derivation from process models using unfolding technique which previously has been used to address the state space explosion when dealing with concurrent behaviors of a Petri net. We reveal and formally describe the equivalence between TAR and Event Adjacency Relation (EAR), the manifestation of TAR in the Complete Prefix Unfolding (CPU) of a Petri net. By computing TARs from CPU using this equivalence, we can alleviate the concurrency caused state-explosion issues. Furthermore, structural boosting rules are categorized, proved and added to the TAR computing algorithm. Formal proofs of correctness and generality of CPU-based TAR computation are provided for the first time by this work, and they significantly expand the range of Petri nets from which TARs can be efficiently derived. Experiments on both industrial and synthesized process models show the effectiveness of proposed CPU-based algorithms as well as the observation that they scale well with the increase in size and concurrency of business process models.