τ-Equivalences for analysis of concurrent systems modelled by Petri nets with silent transitions

The paper is devoted to the investigation of behavioural equivalences for Petri nets with silent transitions (τ-equivalences). Basic τ-equivalences and back-forth τ-bisimulation equivalences are supplemented by new ones, giving rise to the complete set of equivalence notions in interleaving / true concurrency and linear / branching time semantics. Their interrelations are examined for the general Petri nets with silent transitions as well as for the subclass of sequential nets. In addition, the preservation of all the equivalence notions by refinements is investigated.