Semantic Reachability
Raphael Mayr, A ENTCS · Electronic Notes in Theoretical Computer Science · 2000
This paper is an approach to combine the reachability problem with semantic notions like bisimulation equivalence. It deals with questions of the following form: Is there a reachable state that is bisimulation equivalent to a given state ? Here we show some decidability results for process algebras and Petri nets. 1 Introduction The reachability problem plays an important role in the theory of concurrent systems. The question is if a given state is reachable from the initial state by a sequence of actions. The complexity of this problem has been extensively studied (for example it is decidable and EXPSPACE-hard for general Petri nets and NP-complete for Basic Parallel Processes (BPP) [4]). Here we generalize the reachability problem by regarding classes of semantically equivalent states instead of single states. The question is now if a state is reachable (from the initial state) that is a member of a given class. In other words: Is it possible to reach a state that is at least semant...