1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 BRICS, Dept. of Computer Science, University of Aarhus3 unknown4 Department of Computer Science, Science and Technology, Aarhus University5 Department of Computer Science, Science and Technology, Aarhus University
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.
Lecture Notes in Computer Science: Proceedings of the 12th International Conference on Concurrency Theory, 2001, p. 277-291
Transition system; Satisfiability; Automaton; Formal method; System reduction; Petri net; Decidability