|
On the Power of Labels in Transition Systems
Jirí Srba June 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 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.
Available as PostScript, PDF, DVI. |