2011/08/26 by Robert M. Hierons, Robert M Hierons, Hierons, Robert M
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #cs.SE #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1108.5295
arxiv created 2011/08/26 · openalex publication_date 2011/08/26 · arxiv updated 2011/08/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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, called a local trace, is observed at each port. This leads to the environment having reduced observational power: the set of local traces observed need not uniquely define the global trace that occurred. We consider the previously defined implementation relation \sqsubseteqs and start by investigating the problem of defining a language \mathcal L (M) for a multi-port finite state machine (FSM) M such that N \sqsubseteqs M if and only if every global trace of N is in \mathcal L (M). The motivation is that if we can produce such a language \mathcal L (M) then this can potentially be used to inform development and testing. We show that \mathcal L (M) can be uniquely defined but need not be regular. We then prove that it is generally undecidable whether N \sqsubseteqs M, a consequence of this result being that it is undecidable whether there is a test case that is capable of distinguishing two states or two multi-port FSM in distributed testing. This result complements a previous result that it is undecidable whether there is a test case that is guaranteed to distinguish two states or multi-port FSMs. We also give some conditions under which N \sqsubseteqs M is decidable. We then consider the implementation relation \sqsubseteqsk that only concerns input sequences of length k or less. Naturally, given FSMs N and M it is decidable whether N \sqsubseteqsk M since only a finite set of traces is relevant. We prove that if we place bounds on k and the number of ports then we can decide N \sqsubseteqsk M in polynomial time but otherwise this problem is NP-hard.