Deciding Bisimulation and Trace Equivalences for Systems with Many Identical Processes.

In the study of process semantics, trace equivalence and bisimulation equivalence constitute the two extremes of the so-called linear time - branching time spectrum. In this paper, we study the complexity and decidability issues of deciding trace and bisimulation equivalences for the model of systems with many identical processes with respect to various interprocess communication structures. In our model, each system consists of an arbitrary number of identical finite-state processes using Milner's calculus of communicating systems (CCS) as the style of interprocess communication. As it turns out, deciding trace and bisimulation equivalences are undecidable for star-like and linear systems, whereas the two problems are complete for PSPACE and PTIME, respectively, for fully connected systems.