Open AccessOn the Power of Labels in Transition Systems
Author(s) -
Jiřı́ Srba
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i19.21680
Subject(s) - decidability , petri net , reduction (mathematics) , transition system , satisfiability , class (philosophy) , automaton , model checking , discrete mathematics , mathematics , computer science , theoretical computer science , algorithm , artificial intelligence , geometry
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.