Brunel University Research Archive (BURA) >
Schools >
School of Information Systems, Computing and Mathematics >
School of Information Systems, Computing and Mathematics Research Papers >
Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/4075

Title:  Canonical finite state machines for distributed systems 
Authors:  Hierons, RM 
Keywords:  Finite state machine Equivalence Distributed test architecture Canonical 
Publication Date:  2010 
Publisher:  Theoretical Computer Science. 411(2): 566580 
Abstract:  There has been much interest in testing from finite state machines (FSMs) as a result of their suitability for modelling or specifying statebased systems. Where there are multiple ports/interfaces a multiport FSM is used and in testing, a tester is placed at each port. If the testers cannot communicate with one another directly and there is no global clock then we are testing in the distributed test architecture. It is known that the use of the distributed test architecture can affect the power of testing and recent work has characterised this in terms of local sequivalence: in the distributed test architecture we can distinguish two FSMs, such as an implementation and a specification, if and only if they are not locally sequivalent. However, there may be many FSMs that are locally sequivalent to a given FSM and the nature of these FSMs has not been explored. This paper examines the set of FSMs that are locally sequivalent to a given FSM M. It shows that there is a unique smallest FSM χmin(M) and a unique largest FSM χmax(M) that are locally sequivalent to M. Here smallest and largest refer to the set of traces defined by an FSM and thus to its semantics. We also show that for a given FSM M the set of FSMs that are locally sequivalent to M defines a bounded lattice. Finally, we define an FSM that, amongst all FSMs locally sequivalent to M, has fewest states. We thus give three alternative canonical FSMs that are locally sequivalent to an FSM M: one that defines the smallest set of traces, one that defines the largest set of traces, and one with fewest states. All three provide valuable information and the first two can be produced in time that is polynomial in terms of the number of states of M. We prove that the problem of finding an sequivalent FSM with fewest states is NPhard in general but can be solved in polynomial time for the special case where there are two ports. 
URI:  http://bura.brunel.ac.uk/handle/2438/4075 
DOI:  http://dx.doi.org/10.1016/j.tcs.2009.09.039 
ISSN:  03043975 
Appears in Collections:  BSERC Research Papers School of Information Systems, Computing and Mathematics Research Papers Computer Science

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.
