Erratum to: Diagnosis of discrete event systems using decentralized architectures

Erratum to: Discrete Event Dyn Syst

                   DOI 10.1007/s10626-006-0006-8

It was pointed out to us by S. Takai and T. Yamamoto (S. Takai and T. Yamamoto, August 2012. Private communication) that Theorem 9 in the original article Diagnosis of discrete event systems using decentralized architectures was incorrect in that the stated condition for violation of negative codiagnosability is sufficient but not necessary in general. We are very grateful to them for bringing this issue to our attention. The lack of necessity in Theorem 9 also carries over to Theorems 16 and 17 in the original article. In this paper, we explain how to adjust these three theorems so that necessity and sufficiency hold.

In the original article, we called a one-level verifier state (q ₁, l ₁, q ₂, l ₂, q ₃, l ₃) a (l ₁, l ₂, l ₃)-state, and a strongly connected component (SCC) a (l ₁, l ₂, l ₃)-SCC, if every state in the SCC is a (l ₁, l ₂, l ₃)-state. Here, we extend the label l _i to include symbol “?” in addition to “P” and “N”; the new symbol “?” means either “P” or “N”. For example, a (?,P,N)-state can be either a (P,P,N)-state or a (N,P,N)-state. The corrected statements and revised proofs of Theorems 9, 16, and 17 are as follows.

FormalPara Theorem 9

The language generated by system G is not negative-codiagnosable if and only if the one-level verifier V ₁ of G has a path with two SCCs (that may or may not be distinct), a (P,?,N)-SCC and a (?,P,N)-SCC, where each SCC has a transition whose event corresponding to the “P” in the 3-tuple is not ε .

FormalPara Proof

We consider the general case where the two SCCs are distinct. The proof can be straightforwardly adapted to the special case where the two SCCs are the same, i.e., the case of a (P,P,N)-SCC.

• (i) Two SCCs along a path $\Rightarrow$ not negative-codiagnosable.   Without loss of generality, we assume the (P,?,N)-SCC is before the (?,P,N)-SCC along the path. Based on Proposition 7, we can induce a trace triple $s_1 t_1^n u_1 v_1^m, s_2 t_2^n u_2 v_2^m, s t^n u v^m$ from this path, where trace triple (s ₁, s ₂, s) corresponds to the prefix of the path that reaches the (P,?,N)-SCC from the initial state, (t ₁, t ₂, t) corresponds to the edges within the (P,?,N)-SCC, (u ₁,u ₂,u) corresponds to the path from the (P,?,N)-SCC to the (?,P,N)-SCC, and (v ₁,v ₂,v) corresponds to the edges within the (?,P,N)-SCC. We know that s t ⁿ u v ^m must be negative, while s ₁ and $s_2 t_2^n u_2$ are positive. Furthermore, we can select t ₁ and v ₂ such that t ₁, v ₂ ≠ ε. Then the triple $s_1 t_1^n u_1 v_1^m, s_2 t_2^ nu_2 v_2^m, s t^n u v^m$ violates the definition of negative-codiagnosability.

• (ii) Not negative-codiagnosable $\Rightarrow$ two SCCs along a path.   Not negative-codiagnosable implies there exist negative trace u and positive traces s ₁ and s ₂ with arbitrarily long extensions t ₁ and t ₂ such that ${\cal P}_1(u)={\cal P}_1(s_1 t_1)$ and ${\cal P}_2(u)={\cal P}_2(s_2t_2)$. By Proposition 7, these three traces must form a path in V ₁. Since both t ₁ and t ₂ can be arbitrarily long and V ₁ has only a finite number of states, there must be two SCCs corresponding to t ₁ and t ₂, respectively. The SCC corresponding to t ₁ is a (P,?,N)-SCC since s ₁ is positive, and the other corresponding to t ₂ is a (?,P,N)-SCC since s ₂ is positive. Each SCC must have an edge with non-ε corresponding to the “P” component in the 3-tuple in order to induce the arbitrarily long extensions.□

FormalPara Theorem 16

The language generated by system G is not Cond-Disj-Codiag if and only if the two-level verifier V ₂ of G has three SCCs (that may or may not be distinct) along a path, a (N,P,N,?,?)-SCC, a (N,?,N,P,?)-SCC, and a (N,?,N,?,P)-SCC, where each SCC has at least one transition whose event label corresponding to the “P” in the 5-tuple is not ε .

FormalPara Proof

• (i) A path with three SCCs $\Rightarrow$ not conditionally positive-codiagnosable.   Based on Proposition 15, this three-SCC path eventually reaches a (N,P,N,P,P) state. We can induce a 5-tuple trace u ₁, v ₁ w ₁, u ₂, v ₂ w ₂, st from this path, where u ₁, u ₂ are negative, v ₁, v ₂, s are positive, and w ₁, w ₂, t are arbitrarily long. Now, positive trace st is indistinguishable from negative trace u ₁ at site 1 and indistinguishable from negative trace u ₂ at site 2. Furthermore, site 2’s estimate of u ₁ contains a trace with positive prefix v ₁ and site 1’s estimate of u ₂ contains a trace with prefix v ₂. Thus it is not conditionally positive-codiagnosable.

• (ii) Not conditionally positive-codiagnosable $\Rightarrow$ a path with three SCCs.   If the system is not conditionally positive-codiagnosable, then there exist arbitrarily long positive trace st, negative traces u ₁ and u ₂ that have the same projection at site 1 and 2, respectively, and arbitrarily long positive traces v ₁ w ₁ and v ₂ w ₂ such that ${\cal P}_2(u_1)={\cal P}_2(v_1 w_1)$ and ${\cal P}_1(u_2)={\cal P}_1(v_2w_2)$. By Proposition 15, these five traces should form an arbitrarily long path in V ₂. This path must contain three SCCs, (N,P,N,?,?)-SCC, (N,?,N,P,?)-SCC, and (N,?,N,?,P)-SCC, corresponding to arbitrarily long traces v ₁ w ₁, v ₂ w ₂, and s t, respectively. The non-ε edges in each SCC are due to the the non-empty suffixes w ₁, w ₂, and t.□

FormalPara Theorem 17

The language generated by system G is not Cond-Conj-Codiag if and only if the two-level verifier V ₂ of G has two SCCs (that may or may not be distinct) along a path, a (P,N,?,N,N)-SCC and a (?,N,P,N,N)-SCC, where each SCC has at least one transition whose event corresponding to the “P” in the 5-tuple is not ε .

The proof is similar to that of Theorem 16 and omitted.