Issue No. 08 - Aug. (2013 vol. 62)
ISSN: 0018-9340
pp: 1673-1683
Robert M. Hierons , Brunel University,Uxbridge
ABSTRACT
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 $(\sqsubseteq_s)$ and prove that it is undecidable whether $(N \sqsubseteq_{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 \sqsubseteq_{s}M)$ is decidable. We then consider implementation relation $(\sqsubseteq_{s}^k)$ that concerns input sequences of length $(k)$ or less. If we place bounds on $(k)$ and the number of ports then we can decide $(N \sqsubseteq_{s}^{k} M)$ in polynomial time but otherwise this problem is NP-hard.
INDEX TERMS
Automata, Controllability, Polynomials, Computer architecture, distributed test architecture, D2.4: software engineering/software/program verification, D2.5: software engineering/testing and debugging, distributed systems, finite state machine
CITATION
Robert M. Hierons, "Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces", IEEE Transactions on Computers, vol. 62, no. , pp. 1673-1683, Aug. 2013, doi:10.1109/TC.2012.252