Petri Net Reductions for Counting Markings

TL;DR

This paper introduces a structural reduction method for Petri nets that enables counting reachable markings efficiently without enumeration, demonstrated through effective experiments on various models.

Contribution

It presents a novel reduction system that preserves the count of reachable markings, allowing efficient analysis of Petri nets.

Findings

Reductions significantly improve counting efficiency.

Method is effective on a large set of benchmark models.

Reductions preserve the number of reachable markings.

Abstract

We propose a method to count the number of reachable markings of a Petri net without having to enumerate these rst. The method relies on a structural reduction system that reduces the number of places and transitions of the net in such a way that we can faithfully compute the number of reachable markings of the original net from the reduced net and the reduction history. The method has been implemented and computing experiments show that reductions are eective on a large benchmark of models.