Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces

This paper concerns state-based systems that interact with their environment at physically distributed interfaces, called ports. When such a system is used a projection of the global trace, a local trace, is observed at each port. As a result the environment has reduced observational power: the set of local traces observed need not define the global trace that occurred. We consider the previously defined implementation relation ⊆_s and prove that it is undecidable whether N ⊆_s M and so it is also undecidable whether testing can distinguishing two states or FSMs. We also prove that a form of model-checking is undecidable when we have distributed observations and give conditions under which N ⊆_s M is decidable. We then consider implementation relation ⊆_s^k that concerns input sequences of length κ or less. If we place bounds on κ and the number of ports then we can decide N ⊆_s^k M in polynomial time but otherwise this problem is NP-hard.