In: MIT Laboratory for computer Science, Cambridge, MA 02139, USA. 1993.
Abstract: We show that the pomset-trace equivalence problem for finite safe Petri nets is decidable, and is in fact complete for EXPSPACE. We also show that history-preserving bisimulation between such nets is complete for DEXPTIME, settling a question left open by Vogler. Our decision procedures are based on establishing correspondences between bounded-size partial orders of transition firings, from which the upper bounds follow immediately. Lower bounds follow by reduction of corresponding interleaving (languages) equivalence problems with known complexity. Our methods also yield tight complexity bounds for several other true concurrency equivalences. The results are independent of the presence of hidden transitions.