This Article 
 Bibliographic References 
 Add to: 
Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces
Aug. 2013 (vol. 62 no. 8)
pp. 1673-1683
Robert M. Hierons, Brunel University,Uxbridge
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
Robert M. Hierons, "Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces," IEEE Transactions on Computers, vol. 62, no. 8, pp. 1673-1683, Aug. 2013, doi:10.1109/TC.2012.252
Usage of this product signifies your acceptance of the Terms of Use.