Technische Berichte TUD-FI00-11, 41 pages pages, November 2000. Fakultaet Informatik, Technische Universitaet Dresden, Germany.; www.iis.nsk.su/persons/itar/.
Abstract: The paper is devoted to the investigation of behavioral equivalences of concurrent systems modeled by Petri nets with silent transitions. Basic tau-equivalences and back-forth tau-bisimulation equivalences known from the literature are supplemented by new ones, giving rise to complete set of equivalence notions in interleaving / true concurrency and linear / branching time semantics. Their interrelations are examined for the general class of nets as well as for their subclasses of nets without silent transitions and sequential nets (nets without concurrent transitions). In addition, the preservation of all the equivalence notions by refinements (allowing one to consider the systems to be modeled on a lower abstraction levels) is investigated.
Keywords: Petri nets with and without silent transitions; sequential nets; basic and back-forth tau-equivalences; refinement.