In: LNCS 2154: CONCUR 2001 - Concurrency Theory, pages 277-pp. 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings / K. G. Larsen, M. Nielsen (Eds.) --- Springer Verlag, 2001.
Abstract: In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of µ-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.