On the Power of Labels in Transition Systems

13 years 8 months ago
On the Power of Labels in Transition Systems
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.
Jirí Srba
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Authors Jirí Srba
Comments (0)