Undecidability of performance equivalence of Petri nets

TL;DR

This paper proves that checking bisimulation equivalence in Petri nets with durational semantics is generally undecidable, countering previous beliefs that it might be easier than in standard settings.

Contribution

It demonstrates the undecidability of bisimulation equivalence in three out of four durational semantics variants, challenging prior assumptions.

Findings

Undecidability results for three durational semantics variants

Contradicts previous conjecture about tractability in durational Petri nets

Open problem remains for the fourth variant

Abstract

We investigate bisimulation equivalence on Petri nets under durational semantics. Our motivation was to verify the conjecture that in durational setting, the bisimulation equivalence checking problem becomes more tractable than in ordinary setting (which is the case, e.g., over communication-free nets). We disprove this conjecture in three of four proposed variants of durational semantics. The fourth variant remains an intriguing open problem.