On the Power of Labels in Transition Systems

  • Jirí Srba

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 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.
Published
2001-06-04
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