Checking equivalences between concurrent systems of finite agents

Abstract

Consider two synchronously communicating systems p and q over finite agents. Assume that one wants to check whether p ~ q for one of the commonly used equivalences. We show that this question is PSPACE hard for all equivalences which lie between strong bisimulation and trace equivalences. For some equivalences exponential lower and upper bounds are proven. We also show that this problem is NP hard and co-NP hard even for a class of very simple finite agents. Dataflow nets are the simplest systems of asynchronously communicating agents. Let ~ be an equivalence which lies between strong bisimulation and trace equivalences. We show that there is no algorithm for checking ~-equivalence between dataflow nets over finite state agents.