UNIVERSIDADE DE SÃO PAULO - PDF

Description
UNIVERSIDADE DE SÃO PAULO Instituto de Ciências Matemáticas e de Computação ISSN Comments on On minimizing the lengths of checking sequences Adenilso da Silva Simão N ō 307 RELATÓRIOS TÉCNICOS

Please download to get full document.

View again

of 5
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Internet & Web

Publish on:

Views: 38 | Pages: 5

Extension: PDF | Download: 0

Share
Transcript
UNIVERSIDADE DE SÃO PAULO Instituto de Ciências Matemáticas e de Computação ISSN Comments on On minimizing the lengths of checking sequences Adenilso da Silva Simão N ō 307 RELATÓRIOS TÉCNICOS São Carlos - SP Agosto/2007 Comments on On minimizing the lengths of checking sequences Adenilso Simão 1 Instituto de Ciências Matemáticas e de Computação Universidade de São Paulo São Carlos, São Paulo, Brazil Abstract. In [1], Ural et al. propose a sufficient condition for a sequence to be a checking sequence for a complete deterministic FSM. The condition is then used in [1] to elaborate a method for generating checking sequences and it is also used in subsequent improved versions of this method published in [2] and [3]. In this correspondence, we present a counter-example which demonstrates that the condition of the theorem is not sufficient, as it does not address all initialization faults, and show what can be added to make it sufficient. We use definitions from [1]. Let M = (S, X, Y, δ, λ) be a complete deterministic reduced Mealy machine for which there exists a distinguishing sequence D. s 1 is the initial state of M. M is represented as a graph G = (V, E), whose vertices are the states of M (v 1 represents s 1 ) and whose edges are its transitions. A path P = (n 1, n 2 ; x 1 /y 1 )(n 2, n 3 ; x 2 /y 2 ) (n r-1, n r ; x r- 1/y r-1 ) is a finite sequence of adjacent edges in E. The label of P, denoted label(p), is the IO-sequence (x 1 /y 1 )(x 2 /y 2 ) (x r-1 /y r-1 ). P can also be represented by (n 1, n r ; x 1 x 2 x r- 1/y 1 y 2 y r-1 ), and, accordingly, its label can be represented by x 1 x 2 x r-1 /y 1 y 2 y r-1. A transfer sequence T of M from state s i to state s j is the label of a path from s i to s j. Let Q = label(p). A checking sequence of M is an IO-sequence starting at a specific (initial) state of M that distinguishes M from any FSM M * that has at most as many states as M, has the same input and output sets and is not equivalent to M (in the initial state). To formulate a condition for an input sequence to be checking, auxiliary notions of recognition of nodes of P in Q and verification of edges of G in Q are used. (i) n i is d-recognized in Q as some state a of M if (n i, n k ; D/λ(a, D)) is a subpath of P; (ii) if (n q, n i ; T) and (n j, n k ; T) are subpaths of P and D/λ(a, D) is a prefix of T (and, thus, n q and n j are d-recognized in Q as state a of M) and n k is d-recognized in Q as some state a' of M, then n i is t-recognized in Q as state a' of M; (iii) if (n q, n i ; T) and (n j, n k ; T) are subpaths of P such that n q, and n j are either d- recognized or t-recognized in Q as some state a of M and node n k is either d-recognized or t-recognized in Q as some state a' of M, then n i is also t-recognized in Q as state a' of M; (iv) if n i of P is d-recognized or t-recognized in Q (as some state a of M), then n i is recognized in Q (as state a of M). (v) an edge e = (a, b; x/y) of G is verified in Q if there is a subpath (n i,, n i+1 ; x i /y i ) of P such that n i and n i+1 are recognized in Q as states a and b of M, respectively, and x i /y i = x/y. Ural et al. s theorem then states that a sufficient condition for Q to be a checking sequence of M that starts at v 1 is that every edge of G is verified in Q. Theorem 1 [1]. Let Q be an IO-sequence of M starting at v 1 (i.e., the label of a path P = (n 1, n r ; Q) of G) and let D be a distinguishing sequence of M. If every edge (v i, v j ; x/y) of G is verified in Q, then Q is a checking sequence of M. This condition is not sufficient, though. Theorem 2. Given M and an IO-sequence Q that satisfies the condition of Theorem 1, let (n 1, n k ; I/O) be the longest prefix of Q, such that no n i is recognized in Q, for 1 i k 1, and let n k be recognized in Q as state s. If there exists a state s of M, s s 1, such that λ(s, I) = λ(s 1, I) = O and δ(s, I) = δ(s 1, I) = s, then Q is not a checking sequence. Proof. Consider the FSM M in Fig.1, taken from [2]. Consider also two sequences derived in that paper according to Theorem 1. Both sequences start with, followed by the distinguishing sequence D. causes in M a looping transition at state s 1 as well as a transition from state s 2 to s 1. Thus, an FSM M* which produces the same output sequence in response to the input sequence of Q is the FSM M which starts not in s 1, but in state s 2. States s 1 and s 2 are not equivalent, thus M* is not equivalent to M. QED Actually, the problem with the condition of the theorem is that it does not require the starting node of Q be recognized as the initial state s 1 of M. This additional requirement fixes the problem. s 2 s 3 s 5 b/x a/y s 1 a/y b/x s 4 Figure 1. Fig. 2 of [2]. Theorem 3. Let Q be an IO-sequence of M starting at v 1 (i.e., the label of a path P = (n 1, n r ; Q) of G) and let D be a distinguishing sequence of M. If every edge (v i, v j ; x/y) of G is verified in Q and n 1 is d-recognized as s 1 in Q, then Q is a checking sequence of M. Notice that now the longest prefix of Q which has no recognized nodes, as required by Theorem 2, becomes empty. This implies that no state except s 1 could be the initial state of M. Therefore, any initialization fault can be exposed. Based on Theorem 1, Ural et al. elaborate a method for generating minimized checking sequences for complete strongly-connect deterministic FSMs. They reduce the problem of finding a checking sequence into a Rural Chinese Postman problem by deriving a suitable auxiliary graph G' whose paths can be induced in G. These paths are not required to start with the distinguishing sequence, though. As a result, the obtained sequence may not be a checking sequence. The method (and subsequent improvements in [2] and [3]) can be fixed by constraining these paths to start with D/λ(s 1, D). References [1] H. Ural, X. Wu, and F. Zhang. On minimizing the lengths of checking sequences. IEEE Transactions on Computers, 46(1):93-99, [2] R. M. Hierons and H. Ural. Reduced length checking sequences. IEEE Transactions on Computers, 51(9): , [3] R. M. Hierons and H. Ural. Optimizing the length of checking sequences. IEEE Transactions on Computers, 55(5): , 2006.
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks