Issue No. 08 - Aug. (2013 vol. 62)

ISSN: 0018-9340

pp: 1673-1683

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2012.252

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