|
Abstract : |
Abstract We study the following problems for strong and weak bisimulation equivalence: given a labelled Petri net and a finite transition system, are they equivalent?; given a labelled Petri net, is it equivalent to some (unspecified) finite transition system? We show that both problems are decidable for strong bisimulation and undecidable for weak bisimulation. 1 Introduction The decidability of equivalence notions for infinite-state systems has been extensively studied in the last years. Among other results, it has been shown that trace equivalence is undecidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP), while bisimulation equivalence is decidable in both cases [1, 2, 4]., |
