In: Theoretical Computer Science, Vol. 148, No. 2, pages 281-301. 1995.
Abstract: The main result shows the undecidability of (strong) bisimilarity for labeled (place/transition) Petri nets. The technique of the proof applies to the language (or trace) equivalence and the reachability set equality as well, which yields stronger versions with simpler proofs of already known results. The paper also contains two decidability results. One concerns the Petri nets which are deterministic up to bisimilarity, the other concerns semilinear bisimulations and extends the result of Christensen et al. (1993) for basic parallel processes.
Keywords: decidability problems, labeled Petri nets, strong bisimulation.