On the Power of Labels in Transition Systems

  • Jirí Srba


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 mu-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.
How to Cite
Srba, J. (2001). On the Power of Labels in Transition Systems. BRICS Report Series, 8(19). https://doi.org/10.7146/brics.v8i19.21680