PN-BisimInspector: a tool to check Place Bisimilarity in Petri Nets

The verification of behavioral equivalences between concurrent systems is a fundamental challenge in computer science, particularly within the framework of Petri Nets. This thesis focuses on place bisimulation, a behavioral equivalence that ensures two Petri Nets behave the same even if they have different structure. We present BisimInspector, an open-source tool designed to automate the search for place bisimulation relations between Place/Transition Petri Nets. The software implements an algorithmic logic that navigates the state space of potential relations and providing detailed diagnostic feedback in cases of non-equivalence. While the upper bound theoretical complexity of the problem is shown to be O(p^3 · 2^(p^2) · t^2 · kt!), we assume in most practical applications the algorithm remains usable.